aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cases.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/cases.mli')
-rw-r--r--pretyping/cases.mli5
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index ba566f374..ee4148de6 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -114,10 +114,11 @@ 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) ->
+ Environ.env -> Evd.evar_map ref -> glob_constr -> Environ.unsafe_judgment) ->
Environ.env ->
Evd.evar_map ->
(Term.types * tomatch_type) list ->
Context.Rel.t list ->
Constr.constr option ->
- 'a option -> (Evd.evar_map * Names.name list * Term.constr) list
+ glob_constr option ->
+ (Evd.evar_map * Names.name list * Term.constr) list