diff options
| author | letouzey | 2007-07-06 16:35:07 +0000 |
|---|---|---|
| committer | letouzey | 2007-07-06 16:35:07 +0000 |
| commit | 9dec278bb1af17f30021bf0bb04f21682d1f0a3c (patch) | |
| tree | 28bdb13371312f336f37634c9cc6ef6740bea637 /parsing | |
| parent | 4d75ddfdc0382e0d6e163febe12912fe477aa43b (diff) | |
Adding a syntax for "n-ary" rewrite:
rewrite H, H'
means: rewrite H; rewrite H'.
This should still be compatible with other "features" of rewrite: like
orientation, implicit arguments (t:=...), and "in" clause. Concerning
the "in" clause, for the moment only one is allowed at the very end of
the tactic, and it applies to all the different rewrites that are
done. For instance, if someone _really_ wants to use all features at
the same time:
rewrite H1 with (t:=u), <-H2, H3 in *
means: rewrite H1 with (t:=u) in *; rewrite <- H2 in *; rewrite H3 in *
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9954 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 11 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 10 |
2 files changed, 14 insertions, 7 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 3853a6d51c..9d0cd28ff0 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -317,6 +317,9 @@ GEXTEND Gram rename : [ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ] ; + rewriter : + [ [ b = orient; c = constr_with_bindings -> (b,c) ] ] + ; simple_tactic: [ [ (* Basic tactics *) @@ -436,10 +439,10 @@ GEXTEND Gram | IDENT "transitivity"; c = constr -> TacTransitivity c (* Equality and inversion *) - | IDENT "rewrite"; b = orient; c = constr_with_bindings ; cl = clause -> - TacRewrite (b,false,c,cl) - | IDENT "erewrite"; b = orient; c = constr_with_bindings ; cl = clause -> - TacRewrite (b,true,c,cl) + | IDENT "rewrite"; l = LIST1 rewriter SEP ","; cl = clause -> + TacRewrite (false,l,cl) + | IDENT "erewrite"; l = LIST1 rewriter SEP ","; cl = clause -> + TacRewrite (true,l,cl) | IDENT "dependent"; k = [ IDENT "simple"; IDENT "inversion" -> SimpleInversion | IDENT "inversion" -> FullInversion diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index b07213fe98..52b2e5f647 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -824,9 +824,13 @@ and pr_atom1 = function | TacTransitivity c -> str "transitivity" ++ pr_constrarg c (* Equality and inversion *) - | TacRewrite (b,ev,c,cl) -> - hov 1 (str (if ev then "erewrite" else "rewrite") ++ pr_orient b ++ - spc() ++ pr_with_bindings c ++ pr_clauses pr_ident cl) + | TacRewrite (ev,l,cl) -> + hov 1 (str (if ev then "erewrite" else "rewrite") ++ + prlist_with_sep + (fun () -> str ","++spc()) + (fun (b,c) -> pr_orient b ++ spc() ++ pr_with_bindings c) + l + ++ pr_clauses pr_ident cl) | TacInversion (DepInversion (k,c,ids),hyp) -> hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++ pr_quantified_hypothesis hyp ++ |