diff options
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 365276853..c0c4252e6 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -96,7 +96,10 @@ val define_evar_as_product : evar_map -> existential -> evar_map * types val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types val define_evar_as_sort : evar_map -> existential -> evar_map * sorts -val is_unification_pattern : env -> constr -> constr list -> +val is_unification_pattern_evar : env -> existential -> constr list -> + constr -> constr list option + +val is_unification_pattern : env * int -> constr -> constr list -> constr -> constr list option val evar_absorb_arguments : env -> evar_map -> existential -> constr list -> |