diff options
Diffstat (limited to 'pretyping/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index f6052b368..a1323e501 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -15,6 +15,7 @@ open Term open Sign open Libnames open Mod_subst +open Termops (*i*) (* The type of mappings for existential variables. @@ -174,6 +175,8 @@ val meta_reassign : metavariable -> constr * instance_status -> evar_defs -> ev (* [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *) val meta_merge : evar_defs -> evar_defs -> evar_defs +val metas_of : evar_defs -> metamap + (**********************************************************) (* Sort variables *) |