From 9dec278bb1af17f30021bf0bb04f21682d1f0a3c Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 6 Jul 2007 16:35:07 +0000 Subject: 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 --- proofs/tacexpr.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs/tacexpr.ml') diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 8c45d95b3..f99ce1a88 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -185,7 +185,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacTransitivity of 'constr (* Equality and inversion *) - | TacRewrite of bool * evars_flag * 'constr with_bindings * 'id gclause + | TacRewrite of evars_flag * (bool * 'constr with_bindings) list * 'id gclause | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis (* For ML extensions *) -- cgit v1.2.3