1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** This file extends Matching with the main logic for Ltac's
(lazy)match and (lazy)match goal. *)
(** [t] is the type of matching successes. It ultimately contains a
{!Tacexpr.glob_tactic_expr} representing the left-hand side of the
corresponding matching rule, a matching substitution to be
applied, a context substitution mapping identifier to context like
those of {!Constr_matching.matching_result}), and a {!Constr.t}
substitution mapping corresponding to matched hypotheses. *)
type 'a t = {
subst : Constr_matching.bound_ident_map * Ltac_pretype.extended_patvar_map ;
context : Constr_matching.context Names.Id.Map.t;
terms : EConstr.constr Names.Id.Map.t;
lhs : 'a;
}
(** [match_term env sigma term rules] matches the term [term] with the
set of matching rules [rules]. The environment [env] and the
evar_map [sigma] are not currently used, but avoid code
duplication. *)
val match_term :
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
(Constr_matching.binding_bound_vars * Constr_matching.instantiated_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
Tacexpr.glob_tactic_expr t Proofview.tactic
(** [match_goal env sigma hyps concl rules] matches the goal
[hyps|-concl] with the set of matching rules [rules]. The
environment [env] and the evar_map [sigma] are used to check
convertibility for pattern variables shared between hypothesis
patterns or the conclusion pattern. *)
val match_goal:
Environ.env ->
Evd.evar_map ->
EConstr.named_context ->
EConstr.constr ->
(Constr_matching.binding_bound_vars * Constr_matching.instantiated_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
Tacexpr.glob_tactic_expr t Proofview.tactic
|
