From 4dc76691537c57cb8344e82d6bb493360ae12aaa Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 21 Sep 2007 09:42:04 +0000 Subject: - Fixing bug 1703 ("intros until n" falls back on the variable name when the latter is bound to a var which is not a quantified one - this led to remove a line marked "temporary compatibility" ... ; made a distinction between quantified hypothesis as for "intros until" and binding names as in "apply with"; in both cases, we now expect that a identifier not used as a variable, as in "apply f_equal with f:=g" where "f" is a true binder name in f_equal, must not be used as a variable elsewhere [see corresponding change in Ints/Tactic.v]) - Fixing bug 1643 (bug in the algorithm used to possibly reuse a global name in the recursive calls of a coinductive term) - Fixing bug 1699 (bug in contracting nested patterns at printing time when the return clause of the subpatterns is dependent) - Fixing bug 1697 (bug in the TacAssert clause of Tacinterp.subst_tactic) - Fixing bug 1678 (bug in converting constr_pattern to constr in Constrextern) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10131 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Ints/Tactic.v | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'theories/Ints') diff --git a/theories/Ints/Tactic.v b/theories/Ints/Tactic.v index a1654da687..08daffa551 100644 --- a/theories/Ints/Tactic.v +++ b/theories/Ints/Tactic.v @@ -65,16 +65,16 @@ Ltac case_eq name := Ltac eq_tac := match goal with - |- (?f _ = ?f _) => apply f_equal with (f := f) - | |- (?f ?X _ = ?f ?X _) => apply f_equal with (f := f X) - | |- (?f _ _ = ?f _ _) => apply f_equal2 with (f := f) - | |- (?f ?X ?Y _ = ?f ?X ?Y _) => apply f_equal with (f := f X Y) - | |- (?f ?X _ _ = ?f ?X _ _) => apply f_equal2 with (f := f X) - | |- (?f _ _ _ = ?f _ _ _) => apply f_equal3 with (f := f) - | |- (?f ?X ?Y ?Z _ = ?f ?X ?Y ?Z _) => apply f_equal with (f := f X Y Z) - | |- (?f ?X ?Y _ _ = ?f ?X ?Y _ _) => apply f_equal2 with (f := f X Y) - | |- (?f ?X _ _ _ = ?f ?X _ _ _) => apply f_equal3 with (f := f X) - | |- (?f _ _ _ _ _ = ?f _ _ _ _) => apply f_equal4 with (f := f) + |- (?g _ = ?g _) => apply f_equal with (f := g) + | |- (?g ?X _ = ?g ?X _) => apply f_equal with (f := g X) + | |- (?g _ _ = ?g _ _) => apply f_equal2 with (f := g) + | |- (?g ?X ?Y _ = ?g ?X ?Y _) => apply f_equal with (f := g X Y) + | |- (?g ?X _ _ = ?g ?X _ _) => apply f_equal2 with (f := g X) + | |- (?g _ _ _ = ?g _ _ _) => apply f_equal3 with (f := g) + | |- (?g ?X ?Y ?Z _ = ?g ?X ?Y ?Z _) => apply f_equal with (f := g X Y Z) + | |- (?g ?X ?Y _ _ = ?g ?X ?Y _ _) => apply f_equal2 with (f := g X Y) + | |- (?g ?X _ _ _ = ?g ?X _ _ _) => apply f_equal3 with (f := g X) + | |- (?g _ _ _ _ _ = ?g _ _ _ _) => apply f_equal4 with (f := g) end. (************************************** -- cgit v1.2.3