2 files changed, 27 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.