diff options
| author | msozeau | 2008-03-07 16:32:12 +0000 |
|---|---|---|
| committer | msozeau | 2008-03-07 16:32:12 +0000 |
| commit | ec850ff623801e514b3ed0a42beb6f7984992520 (patch) | |
| tree | 6a03dd3d0545b927326f28e7d8da08a850cead5f /tactics/equality.ml | |
| parent | 905c47d6a07cc69b9e7aa0b9d73caeacf2b1d2be (diff) | |
Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part
of the fix I added an optional "by" annotation for rewrite to solve said
conditions in the same tactic call. Most of the theories have been
updated, only FSets is missing, Pierre will take care of it.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10634 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 93b555b34d..214389f18f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -175,8 +175,13 @@ let general_multi_rewrite l2r with_evars c cl = (general_rewrite_ebindings l2r c with_evars) do_hyps -let general_multi_multi_rewrite with_evars l cl = - let do1 l2r c = general_multi_rewrite l2r with_evars c cl in +let general_multi_multi_rewrite with_evars l cl tac = + let do1 l2r c = + match tac with + None -> general_multi_rewrite l2r with_evars c cl + | Some tac -> tclTHENSFIRSTn (general_multi_rewrite l2r with_evars c cl) + [|tclIDTAC|] (tclCOMPLETE tac) + in let rec doN l2r c = function | Precisely n when n <= 0 -> tclIDTAC | Precisely 1 -> do1 l2r c |