diff options
Diffstat (limited to 'proofs/tacexpr.ml')
| -rw-r--r-- | proofs/tacexpr.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 1808fd3aac..f3152f3314 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -117,11 +117,12 @@ type pattern_expr = constr_expr (* Type of patterns *) type 'a match_pattern = | Term of 'a - | Subterm of identifier option * 'a + | Subterm of bool * identifier option * 'a (* Type of hypotheses for a Match Context rule *) type 'a match_context_hyps = | Hyp of name located * 'a match_pattern + | Def of name located * 'a match_pattern * 'a match_pattern (* Type of a Match rule for Match Context and Match *) type ('a,'t) match_rule = |