diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-03-24 02:18:53 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-06-09 16:43:49 +0200 |
| commit | f713e6c195d1de177b43cab7c2902f5160f6af9f (patch) | |
| tree | 87cab142f23b01559096dce1c9bb0493d9717553 /pretyping/cases.mli | |
| parent | 3e1f527a50142a5c73ead24e3fcdb6e2ac9f50e5 (diff) | |
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".
Diffstat (limited to 'pretyping/cases.mli')
| -rw-r--r-- | pretyping/cases.mli | 13 |
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 |