diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-30 12:02:32 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-30 12:02:32 +0000 |
| commit | 306d1be283442c361aa26d000d339f3f4dfbeab9 (patch) | |
| tree | 5fdec06c70ef551f8b775988820fb07c7538e29f /tactics/hiddentac.ml | |
| 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 'tactics/hiddentac.ml')
| -rw-r--r-- | tactics/hiddentac.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index ba17ac30c..756212f0a 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -111,9 +111,8 @@ let h_simplest_right = h_right false NoBindings (* Conversion *) let h_reduce r cl = abstract_tactic (TacReduce (r,cl)) (reduce r cl) -let h_change oc c cl = - abstract_tactic (TacChange (oc,c,cl)) - (change (Option.map Redexpr.out_with_occurrences oc) c cl) +let h_change op c cl = + abstract_tactic (TacChange (op,c,cl)) (change op c cl) (* Equivalence relations *) let h_reflexivity = abstract_tactic TacReflexivity intros_reflexivity |