- 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

1 files changed, 10 insertions, 10 deletions

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.
 
 (**************************************