22 files changed, 239 insertions, 5 deletions
diff --git a/test-suite/bugs/closed/1501.v b/test-suite/bugs/closed/1501.v
new file mode 100644
index 000000000..e771e192d
--- /dev/null
+++ b/test-suite/bugs/closed/1501.v
@@ -0,0 +1,67 @@
+Set Implicit Arguments.
+
+
+Require Export Relation_Definitions.
+Require Export Setoid.
+Require Import Morphisms.
+
+
+Section Essais.
+
+(* Parametrized Setoid *)
+Parameter K : Type -> Type.
+Parameter equiv : forall A : Type, K A -> K A -> Prop.
+Parameter equiv_refl : forall (A : Type) (x : K A), equiv x x.
+Parameter equiv_sym : forall (A : Type) (x y : K A), equiv x y -> equiv y x.
+Parameter equiv_trans : forall (A : Type) (x y z : K A), equiv x y -> equiv y z
+-> equiv x z.
+
+(* basic operations *)
+Parameter val : forall A : Type, A -> K A.
+Parameter bind : forall A B : Type, K A -> (A -> K B) -> K B.
+
+Parameter
+  bind_compat :
+    forall (A B : Type) (m1 m2 : K A) (f1 f2 : A -> K B),
+    equiv m1 m2 ->
+    (forall x : A, equiv (f1 x) (f2 x)) -> equiv (bind m1 f1) (bind m2 f2).
+
+(* monad axioms *)
+Parameter
+  bind_val_l :
+    forall (A B : Type) (a : A) (f : A -> K B), equiv (bind (val a) f) (f a).
+Parameter
+  bind_val_r :
+    forall (A : Type) (m : K A), equiv (bind m (fun a => val a)) m.
+Parameter
+  bind_assoc :
+    forall (A B C : Type) (m : K A) (f : A -> K B) (g : B -> K C),
+    equiv (bind (bind m f) g) (bind m (fun a => bind (f a) g)).
+
+
+Hint Resolve equiv_refl equiv_sym equiv_trans: monad.
+
+Add Parametric Relation A : (K A) (@equiv A)
+    reflexivity proved by (@equiv_refl A)
+    symmetry proved by (@equiv_sym A)
+    transitivity proved by (@equiv_trans A)
+      as equiv_rel.
+
+Add Parametric Morphism A B : (@bind A B)
+    with signature (@equiv A) ==> (pointwise_relation A (@equiv B)) ==> (@equiv B)
+      as bind_mor.
+Proof.
+  unfold pointwise_relation; intros; apply bind_compat; auto.
+Qed.
+
+Lemma test:
+  forall (A B: Type) (m1 m2 m3: K A) (f: A -> A -> K B),
+    (equiv m1 m2) -> (equiv m2 m3) ->
+    equiv (bind m1 (fun a => bind m2 (fun a' => f a a')))
+          (bind m2 (fun a => bind m3 (fun a' => f a a'))).
+Proof.
+  intros A B m1 m2 m3 f H1 H2.
+  setoid_rewrite H1. (* this works *)
+  setoid_rewrite H2.
+  reflexivity.
+Qed.
diff --git a/test-suite/bugs/closed/2001.v b/test-suite/bugs/closed/2001.v
index d0b3bf173..652c65706 100644
--- a/test-suite/bugs/closed/2001.v
+++ b/test-suite/bugs/closed/2001.v
@@ -7,7 +7,7 @@ Inductive T : Set :=
 | v : T.
 
 Definition f (s:nat) (t:T) : nat.
-fix 2.
+fix f 2.
 intros s t.
 refine
   match t with
diff --git a/test-suite/bugs/closed/2456.v b/test-suite/bugs/closed/2456.v
new file mode 100644
index 000000000..e5a392c4d
--- /dev/null
+++ b/test-suite/bugs/closed/2456.v
@@ -0,0 +1,58 @@
+
+Require Import Equality.
+
+Parameter Patch : nat -> nat -> Set.
+
+Inductive Catch (from to : nat) : Type
+    := MkCatch : forall (p : Patch from to),
+                 Catch from to.
+Arguments MkCatch [from to].
+
+Inductive CatchCommute5
+        : forall {from mid1 mid2 to : nat},
+          Catch from mid1
+       -> Catch mid1 to
+       -> Catch from mid2
+       -> Catch mid2 to
+       -> Prop
+     := MkCatchCommute5 :
+           forall {from mid1 mid2 to : nat}
+                  (p : Patch from mid1)
+                  (q : Patch mid1 to)
+                  (q' : Patch from mid2)
+                  (p' : Patch mid2 to),
+           CatchCommute5 (MkCatch p) (MkCatch q) (MkCatch q') (MkCatch p').
+
+Inductive CatchCommute {from mid1 mid2 to : nat}
+                       (p : Catch from mid1)
+                       (q : Catch mid1 to)
+                       (q' : Catch from mid2)
+                       (p' : Catch mid2 to)
+                     : Prop
+    := isCatchCommute5 : forall (catchCommuteDetails : CatchCommute5 p q q' p'),
+                         CatchCommute p q q' p'.
+Notation "<< p , q >> <~> << q' , p' >>"
+    := (CatchCommute p q q' p')
+    (at level 60, no associativity).
+
+Lemma CatchCommuteUnique2 :
+      forall {from mid mid' to : nat}
+             {p   : Catch from mid}  {q   : Catch mid  to}
+             {q'  : Catch from mid'} {p'  : Catch mid' to}
+             {q'' : Catch from mid'} {p'' : Catch mid' to}
+             (commute1 : <<p, q>> <~> <<q', p'>>)
+             (commute2 : <<p, q>> <~> <<q'', p''>>),
+      (p' = p'') /\ (q' = q'').
+Proof with auto.
+intros.
+set (X := commute2).
+Fail dependent destruction commute1;
+dependent destruction catchCommuteDetails;
+dependent destruction commute2;
+dependent destruction catchCommuteDetails generalizing X.
+revert X.
+dependent destruction commute1;
+dependent destruction catchCommuteDetails;
+dependent destruction commute2;
+dependent destruction catchCommuteDetails.
+Abort.
diff --git a/test-suite/bugs/closed/2814.v b/test-suite/bugs/closed/2814.v
new file mode 100644
index 000000000..99da1e3e4
--- /dev/null
+++ b/test-suite/bugs/closed/2814.v
@@ -0,0 +1,6 @@
+Require Import Program.
+
+Goal forall (x : Type) (f g : Type -> Type) (H : f x ~= g x), False.
+  intros.
+  Fail induction H.
+Abort.
diff --git a/test-suite/bugs/closed/2969.v b/test-suite/bugs/closed/2969.v
index a03adbd73..7b1a26178 100644
--- a/test-suite/bugs/closed/2969.v
+++ b/test-suite/bugs/closed/2969.v
@@ -12,6 +12,7 @@ eexists.
 reflexivity.
 Grab Existential Variables.
 admit.
+Admitted.
 
 (* Alternative variant which failed but without raising anomaly *)
 
@@ -24,3 +25,4 @@ clearbody n n0.
 exact I.
 Grab Existential Variables.
 admit.
+Admitted.
diff --git a/test-suite/bugs/closed/3100.v b/test-suite/bugs/closed/3100.v
new file mode 100644
index 000000000..6f35a74dc
--- /dev/null
+++ b/test-suite/bugs/closed/3100.v
@@ -0,0 +1,9 @@
+Fixpoint F (n : nat) (A : Type) : Type :=
+  match n with
+  | 0 => True
+  | S n => forall (x : A), F n (x = x)
+  end.
+
+Goal forall A n, (forall (x : A) (e : x = x), F n (e = e)).
+intros A n.
+Fail change (forall x, F n (x = x)) with (F (S n)).
diff --git a/test-suite/bugs/closed/3230.v b/test-suite/bugs/closed/3230.v
new file mode 100644
index 000000000..265310b1a
--- /dev/null
+++ b/test-suite/bugs/closed/3230.v
@@ -0,0 +1,14 @@
+Structure type : Type := Pack { ob : Type }.
+Polymorphic Record category := { foo : Type }.
+Definition FuncComp := Pack category.
+Axiom C : category.
+
+Check (C : ob FuncComp). (* OK *)
+
+Canonical Structure FuncComp.
+
+Check (C : ob FuncComp).
+(* Toplevel input, characters 15-39:
+Error:
+The term "C" has type "category" while it is expected to have type
+ "ob FuncComp". *)
diff --git a/test-suite/bugs/closed/3320.v b/test-suite/bugs/closed/3320.v
new file mode 100644
index 000000000..a5c243d8e
--- /dev/null
+++ b/test-suite/bugs/closed/3320.v
@@ -0,0 +1,5 @@
+Goal forall x : nat, True.
+  fix goal 1.
+  assumption.
+Fail Qed.
+Undo.
diff --git a/test-suite/bugs/closed/3350.v b/test-suite/bugs/closed/3350.v
index c041c401f..c1ff292b3 100644
--- a/test-suite/bugs/closed/3350.v
+++ b/test-suite/bugs/closed/3350.v
@@ -55,7 +55,7 @@ Lemma lower_ind (P: forall n (p i:Fin.t (S n)), option (Fin.t n) -> Prop)
                 P (S n) (Fin.FS p) (Fin.FS i) None) :
   forall n (p i:Fin.t (S n)), P n p i (lower p i).
 Proof.
-  fix 2. intros n p.
+  fix lower_ind 2. intros n p.
   refine (match p as p1 in Fin.t (S n1)
                 return forall (i1:Fin.t (S n1)), P n1 p1 i1 (lower p1 i1)
           with
diff --git a/test-suite/bugs/closed/3377.v b/test-suite/bugs/closed/3377.v
index 8e9e3933c..abfcf1d35 100644
--- a/test-suite/bugs/closed/3377.v
+++ b/test-suite/bugs/closed/3377.v
@@ -5,6 +5,7 @@ Record prod A B := pair { fst : A; snd : B}.
 Goal fst (@pair Type Type Type Type).
 Set Printing All.
 match goal with |- ?f ?x => set (foo := f x) end.
+Abort.
 
 Goal forall x : prod Set Set, x = @pair _ _ (fst x) (snd x).
 Proof.
@@ -12,6 +13,6 @@ Proof.
   lazymatch goal with
     | [ |- ?x = @pair _ _ (?f ?x) (?g ?x) ] => pose f
   end.
-
 (* Toplevel input, characters 7-44:
 Error: No matching clauses for match. *)
+Abort.
diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v
index 606c6e084..668f6bb42 100644
--- a/test-suite/bugs/closed/4069.v
+++ b/test-suite/bugs/closed/4069.v
@@ -41,6 +41,8 @@ Proof. f_equal.
   8.5: 2 goals, skipn n l = l -> k ++ skipn n l = skipn n l
     and skipn n l = l
 *)
+Abort.
+
 Require Import List.
 Fixpoint replicate {A} (n : nat) (x : A) : list A :=
   match n with 0 => nil | S n => x :: replicate n x end.
diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v
index eb37141bc..28800ac05 100644
--- a/test-suite/bugs/closed/4198.v
+++ b/test-suite/bugs/closed/4198.v
@@ -13,6 +13,7 @@ Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'),
   match goal with
     | [ |- context G[@hd] ] => idtac
   end.
+Abort.
 
 (* This second example comes from CFGV where inspecting subterms of a
    match is expecting to inspect first the term to match (even though
@@ -35,3 +36,4 @@ Ltac mydestruct :=
 Goal forall x, match x with 0 => 0 | _ => 0 end = 0.
 intros.
 mydestruct.
+Abort.
diff --git a/test-suite/bugs/closed/4403.v b/test-suite/bugs/closed/4403.v
new file mode 100644
index 000000000..a80f38fe2
--- /dev/null
+++ b/test-suite/bugs/closed/4403.v
@@ -0,0 +1,3 @@
+(* -*- coq-prog-args: ("-type-in-type"); -*- *)
+
+Definition some_prop : Prop := Type.
diff --git a/test-suite/bugs/closed/4722.v b/test-suite/bugs/closed/4722.v
deleted file mode 100644
index 2d41828f1..000000000
--- a/test-suite/bugs/closed/4722.v
+++ /dev/null
@@ -1 +0,0 @@
-(* -*- coq-prog-args: ("-R" "4722" "Foo") -*- *)
diff --git a/test-suite/bugs/closed/4722/tata b/test-suite/bugs/closed/4722/tata
deleted file mode 120000
index b38e66e75..000000000
--- a/test-suite/bugs/closed/4722/tata
+++ /dev/null
@@ -1 +0,0 @@
-toto
-\ No newline at end of file
diff --git a/test-suite/bugs/closed/4782.v b/test-suite/bugs/closed/4782.v
index dbd71035d..1e1a4cb9c 100644
--- a/test-suite/bugs/closed/4782.v
+++ b/test-suite/bugs/closed/4782.v
@@ -6,6 +6,7 @@ Inductive p : Prop := consp : forall (e : r) (x : type e), cond e x -> p.
 
 Goal p.
 Fail apply consp with (fun _ : bool => mk_r unit (fun x => True)) nil.
+Abort.
  
 (* A simplification of an example from coquelicot, which was failing
    at some time after a fix #4782 was committed. *)
@@ -21,4 +22,5 @@ Set Typeclasses Debug.
 Goal forall (A:T) (x:dom A), pairT A A = pairT A A.
 intros.
 apply (F _ _)  with (x,x).
+Abort.
   
diff --git a/test-suite/bugs/closed/6951.v b/test-suite/bugs/closed/6951.v
new file mode 100644
index 000000000..419f8d7c4
--- /dev/null
+++ b/test-suite/bugs/closed/6951.v
@@ -0,0 +1,2 @@
+Record float2 : Set := Float2 { Fnum : unit }.
+Scheme Equality for float2.
diff --git a/test-suite/bugs/closed/6956.v b/test-suite/bugs/closed/6956.v
new file mode 100644
index 000000000..ee21adbbf
--- /dev/null
+++ b/test-suite/bugs/closed/6956.v
@@ -0,0 +1,13 @@
+(** Used to trigger an anomaly with VM compilation *)
+
+Set Universe Polymorphism.
+
+Inductive t A : nat -> Type :=
+| nil : t A 0
+| cons : forall (h : A) (n : nat), t A n -> t A (S n).
+
+Definition case0 {A} (P : t A 0 -> Type) (H : P (nil A)) v : P v :=
+match v with
+| nil _ => H
+| _ => fun devil => False_ind (@IDProp) devil
+end.
diff --git a/test-suite/bugs/closed/7011.v b/test-suite/bugs/closed/7011.v
new file mode 100644
index 000000000..296e4e11e
--- /dev/null
+++ b/test-suite/bugs/closed/7011.v
@@ -0,0 +1,16 @@
+(* Fix and Cofix were missing in tactic unification *)
+
+Goal exists e, (fix foo (n : nat) : nat := match n with O => e | S n' => foo n' end)
+               = (fix foo (n : nat) : nat := match n with O => O | S n' => foo n' end).
+Proof.
+  eexists.
+  reflexivity.
+Qed.
+
+CoInductive stream := cons : nat -> stream -> stream.
+
+Goal exists e, (cofix foo := cons e foo) = (cofix foo := cons 0 foo).
+Proof.
+  eexists.
+  reflexivity.
+Qed.
diff --git a/test-suite/bugs/closed/7392.v b/test-suite/bugs/closed/7392.v
new file mode 100644
index 000000000..cf465c658
--- /dev/null
+++ b/test-suite/bugs/closed/7392.v
@@ -0,0 +1,9 @@
+Inductive R : nat -> Prop := ER : forall n, R n -> R (S n).
+
+Goal (forall (n : nat), R n -> False) -> True -> False.
+Proof.
+intros H0 H1.
+eapply H0.
+clear H1.
+apply ER.
+simpl.
diff --git a/test-suite/bugs/closed/7462.v b/test-suite/bugs/closed/7462.v
new file mode 100644
index 000000000..40ca39e38
--- /dev/null
+++ b/test-suite/bugs/closed/7462.v
@@ -0,0 +1,13 @@
+(* Adding an only-printing notation should not override existing
+   interpretations for the same notation. *)
+
+Notation "$ x" := (@id nat x) (only parsing, at level 0).
+Notation "$ x" := (@id bool x) (only printing, at level 0).
+Check $1. (* Was: Error: Unknown interpretation for notation "$ _". *)
+
+(* Adding an only-printing notation should not let believe
+   that a parsing rule has been given *)
+
+Notation "$ x" := (@id bool x) (only printing, at level 0).
+Notation "$ x" := (@id nat x) (only parsing, at level 0).
+Check $1. (* Was: Error: Syntax Error: Lexer: Undefined token *)
diff --git a/test-suite/bugs/closed/7554.v b/test-suite/bugs/closed/7554.v
new file mode 100644
index 000000000..12b0aa2cb
--- /dev/null
+++ b/test-suite/bugs/closed/7554.v
@@ -0,0 +1,12 @@
+Require Import Coq.Program.Tactics.
+
+(* these should not result in anomalies *)
+
+Fail Program Lemma foo:
+  forall P, forall H, forall (n:nat), P n.
+
+Fail Program Lemma foo:
+  forall a (P : list a -> Prop), forall H, forall (n:list a), P n.
+
+Fail Program Lemma foo:
+  forall (a : Type) (P : list a -> Prop), forall H, forall (n:list a), P n.