From f713e6c195d1de177b43cab7c2902f5160f6af9f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 24 Mar 2017 02:18:53 +0100 Subject: A fix to #5414 (ident bound by ltac names now known for "match"). Also taking into account a name in the return clause and in the indices. Note the double meaning ``bound as a term to match'' and ``binding in the "as" clause'' when the term to match is a variable for all of "match", "if" and "let". --- pretyping/cases.mli | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) (limited to 'pretyping/cases.mli') 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 -- cgit v1.2.3