diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 12 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 5 |
2 files changed, 11 insertions, 6 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 diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index da915a5cc3..448b78e262 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -821,14 +821,15 @@ and pr_atom1 = function | TacTransitivity c -> str "transitivity" ++ pr_constrarg c (* Equality and inversion *) - | TacRewrite (ev,l,cl) -> + | TacRewrite (ev,l,cl,by) -> hov 1 (str (if ev then "erewrite" else "rewrite") ++ prlist_with_sep (fun () -> str ","++spc()) (fun (b,m,c) -> pr_orient b ++ spc() ++ pr_multi m ++ pr_with_bindings c) l - ++ pr_clauses pr_ident cl) + ++ pr_clauses pr_ident cl + ++ (match by with Some by -> pr_by_tactic (pr_tac_level ltop) by | None -> mt())) | TacInversion (DepInversion (k,c,ids),hyp) -> hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++ pr_quantified_hypothesis hyp ++ |