diff options
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 4fce79be2..9ba82bf1f 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -57,6 +57,10 @@ val ise_try : evar_defs -> (unit -> bool) list -> bool val ise_undefined : evar_defs -> constr -> bool val has_undefined_isevars : evar_defs -> constr -> bool +val new_isevar_sign : + Environ.env -> Evd.evar_map -> Term.constr -> Term.constr list -> + Evd.evar_map * Term.constr + val new_isevar : evar_defs -> env -> loc * hole_kind -> constr -> constr val is_eliminator : constr -> bool |