diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.mli | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 70fa945ff1..d875edd796 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -110,3 +110,14 @@ type 'a pattern_matching_problem = val compile : 'a pattern_matching_problem -> Environ.unsafe_judgment + +val prepare_predicate : Loc.t -> + (Evarutil.type_constraint -> + Environ.env -> Evd.evar_map ref -> 'a -> Environ.unsafe_judgment) -> + Evd.evar_map -> + Environ.env -> + (Term.types * tomatch_type) list -> + Context.rel_context list -> + Constr.constr option -> + 'a option -> (Evd.evar_map * Names.name list * Term.constr) list + |