- 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

4 files changed, 56 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/shouldfail/1703.v b/test-suite/bugs/closed/shouldfail/1703.v
new file mode 100644
index 0000000000..6b5198cc03
--- /dev/null
+++ b/test-suite/bugs/closed/shouldfail/1703.v
@@ -0,0 +1,7 @@
+(* Check correct binding of intros until used in Ltac *)
+
+Ltac intros_until n := intros until n.
+
+Goal forall i j m n : nat, i = 0 /\ j = 0 /\ m = 0 /\ n = 0.
+intro i.
+intros until i.
diff --git a/test-suite/bugs/closed/shouldsucceed/1643.v b/test-suite/bugs/closed/shouldsucceed/1643.v
new file mode 100644
index 0000000000..6ecbc810b7
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1643.v
@@ -0,0 +1,20 @@
+(* Check some aspects of that the algorithm used to possibly reuse a
+   global name in the recursive calls (coinductive case) *)
+
+CoInductive Str : Set := Cons (h:nat) (t:Str).
+
+Definition decomp_func (s:Str) :=
+   match s with
+   | Cons h t => Cons h t
+   end.
+
+Theorem decomp s: s = decomp_func s.
+Proof.
+intros s.
+case s; simpl; reflexivity.
+Qed.
+
+Definition zeros := (cofix z : Str := Cons 0 z).
+Lemma zeros_rw : zeros = Cons 0 zeros.
+rewrite (decomp zeros).
+simpl.
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index a3033e94fc..3c440b9d02 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -7,3 +7,16 @@ fix F (t : t) : P t :=
      : forall P : t -> Type,
        (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
 
+proj = 
+fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) =>
+match eq_nat_dec x y with
+| left eqprf =>
+    match eqprf in (_ = z) return (P z) with
+    | refl_equal => def
+    end
+| right _ => prf
+end
+     : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
+
+
+Argument scopes are [nat_scope nat_scope _ _ _]
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 452d360362..56d5cfb4e7 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -4,3 +4,19 @@ Inductive t : Set :=
     k : let x := t in x -> x.
 
 Print t_rect.
+
+(* Do not contract nested patterns with dependent return type *)
+(* see bug #1699 *)
+
+Require Import Arith.
+
+Definition proj (x y:nat) (P:nat -> Type) (def:P x) (prf:P y) : P y :=
+  match eq_nat_dec x y return P y with
+  | left eqprf => 
+    match eqprf in (_ = z) return (P z) with
+    | refl_equal => def
+    end
+  | _ => prf
+ end.
+
+Print proj.