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 /parsing/g_tactic.ml4 | |
| 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 'parsing/g_tactic.ml4')
| -rw-r--r-- | parsing/g_tactic.ml4 | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index a4e5d4cb83..96db00e3e4 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -319,6 +319,10 @@ GEXTEND Gram [ [ IDENT "by"; tac = tactic_expr LEVEL "3" -> TacComplete tac | -> TacId [] ] ] ; + opt_by_tactic: + [ [ IDENT "by"; tac = tactic_expr LEVEL "3" -> Some tac + | -> None ] ] + ; rename : [ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ] ; @@ -471,10 +475,10 @@ GEXTEND Gram | IDENT "transitivity"; c = constr -> TacTransitivity c (* Equality and inversion *) - | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause -> - TacRewrite (false,l,cl) - | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause -> - TacRewrite (true,l,cl) + | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause; t=opt_by_tactic -> + TacRewrite (false,l,cl,t) + | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause; t=opt_by_tactic -> + TacRewrite (true,l,cl,t) | IDENT "dependent"; k = [ IDENT "simple"; IDENT "inversion" -> SimpleInversion | IDENT "inversion" -> FullInversion |