aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cases.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/cases.mli')
-rw-r--r--pretyping/cases.mli13
1 files changed, 9 insertions, 4 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index b16342db4..4b1fde25a 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -39,9 +39,9 @@ val irrefutable : env -> cases_pattern -> bool
val compile_cases :
?loc:Loc.t -> case_style ->
- (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref ->
+ (type_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) * evar_map ref ->
type_constraint ->
- env -> glob_constr option * tomatch_tuples * cases_clauses ->
+ env -> ltac_var_map -> glob_constr option * tomatch_tuples * cases_clauses ->
unsafe_judgment
val constr_of_pat :
@@ -101,6 +101,7 @@ and pattern_continuation =
type 'a pattern_matching_problem =
{ env : env;
+ lvar : Glob_term.ltac_var_map;
evdref : evar_map ref;
pred : constr;
tomatch : tomatch_stack;
@@ -115,10 +116,14 @@ val compile : 'a pattern_matching_problem -> unsafe_judgment
val prepare_predicate : ?loc:Loc.t ->
(Evarutil.type_constraint ->
- Environ.env -> Evd.evar_map ref -> glob_constr -> unsafe_judgment) ->
+ Environ.env -> Evd.evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) ->
Environ.env ->
Evd.evar_map ->
+ Glob_term.ltac_var_map ->
(types * tomatch_type) list ->
- rel_context list ->
+ (rel_context * rel_context) list ->
constr option ->
glob_constr option -> (Evd.evar_map * Names.name list * constr) list
+
+val make_return_predicate_ltac_lvar : Evd.evar_map -> Names.name ->
+ Glob_term.glob_constr -> constr -> Glob_term.ltac_var_map -> Glob_term.ltac_var_map