diff options
| author | herbelin | 2009-12-30 12:02:32 +0000 |
|---|---|---|
| committer | herbelin | 2009-12-30 12:02:32 +0000 |
| commit | 306d1be283442c361aa26d000d339f3f4dfbeab9 (patch) | |
| tree | 5fdec06c70ef551f8b775988820fb07c7538e29f /proofs | |
| parent | 77d86619f5f557de52a391f6811bacd73c01580b (diff) | |
Fixing bug #2146 (broken selection of occurrences in "change").
In trunk the different possible combinations of "at" and "in" with
occurrences are taken into account.
In 8.2 branch, it remains fragile (syntaxes that were accepted remain
accepted and a message warns if the occurrences coming after the
"with" are not taken into account).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12614 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacexpr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index d16ad78bac..b56e5184e0 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -205,7 +205,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr = (* Conversion *) | TacReduce of ('constr,'cst,'pat) red_expr_gen * 'id gclause - | TacChange of 'pat with_occurrences option * 'constr * 'id gclause + | TacChange of 'pat option * 'constr * 'id gclause (* Equivalence relations *) | TacReflexivity |