metaprogramming-rosetta-stone
metaprogramming-rosetta-stone copied to clipboard
Loosen autoinduct Ltac assumptions if possible; otherwise document