null_meta : term list * instantiation
Empty metavariable information.
This is a pair consisting of an empty list of terms and a null instantiation
(see null_inst). It is used inside most tactics to indicate that they do
nothing interesting with metavariables.
- FAILURE CONDITIONS
This is not intended for general use, but readers writing custom tactics from
scratch may find it convenient.
- SEE ALSO