diff options
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 1831110a7..e8669e5fa 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -61,9 +61,10 @@ val evar_define : (***********************************************************) (* Evars/Metas switching... *) -(* [exist_to_meta] generates new metavariables for each existential - and performs the replacement in the given constr *) -val exist_to_meta : evar_map -> open_constr -> (Termops.metamap * constr) +(* [evars_to_metas] generates new metavariables for each non dependent + existential and performs the replacement in the given constr; it also + returns the evar_map extended with dependent evars *) +val evars_to_metas : evar_map -> open_constr -> (evar_map * constr) val non_instantiated : evar_map -> (evar * evar_info) list |