From a511dbb827b556077fe19c28d0c6c43a6afe387d Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 23 Oct 2017 11:49:42 +0200
Subject: Move bug files to match their new GitHub ID (fixes #6001).

---
 test-suite/bugs/closed/1100.v |  12 ---
 test-suite/bugs/closed/121.v  |  17 ----
 test-suite/bugs/closed/1238.v |  22 +++++
 test-suite/bugs/closed/1341.v |  17 ++++
 test-suite/bugs/closed/1362.v |  26 ++++++
 test-suite/bugs/closed/148.v  |  26 ------
 test-suite/bugs/closed/1542.v |  40 ++++++++
 test-suite/bugs/closed/1543.v | 100 ++++++++++++++++++++
 test-suite/bugs/closed/1545.v |  20 ++++
 test-suite/bugs/closed/1547.v |   5 +
 test-suite/bugs/closed/1551.v |  13 +++
 test-suite/bugs/closed/1584.v |   5 +
 test-suite/bugs/closed/328.v  |  40 --------
 test-suite/bugs/closed/329.v  | 100 --------------------
 test-suite/bugs/closed/331.v  |  20 ----
 test-suite/bugs/closed/335.v  |   5 -
 test-suite/bugs/closed/348.v  |  13 ---
 test-suite/bugs/closed/38.v   |  22 -----
 test-suite/bugs/closed/545.v  |   5 -
 test-suite/bugs/closed/5797.v | 213 ++++++++++++++++++++++++++++++++++++++++++
 test-suite/bugs/closed/5845.v |   7 ++
 test-suite/bugs/closed/5940.v |  12 +++
 test-suite/bugs/closed/846.v  | 213 ------------------------------------------
 test-suite/bugs/closed/931.v  |   7 --
 test-suite/bugs/opened/1615.v |  12 +++
 test-suite/bugs/opened/743.v  |  12 ---
 26 files changed, 492 insertions(+), 492 deletions(-)
 delete mode 100644 test-suite/bugs/closed/1100.v
 delete mode 100644 test-suite/bugs/closed/121.v
 create mode 100644 test-suite/bugs/closed/1238.v
 create mode 100644 test-suite/bugs/closed/1341.v
 create mode 100644 test-suite/bugs/closed/1362.v
 delete mode 100644 test-suite/bugs/closed/148.v
 create mode 100644 test-suite/bugs/closed/1542.v
 create mode 100644 test-suite/bugs/closed/1543.v
 create mode 100644 test-suite/bugs/closed/1545.v
 create mode 100644 test-suite/bugs/closed/1547.v
 create mode 100644 test-suite/bugs/closed/1551.v
 create mode 100644 test-suite/bugs/closed/1584.v
 delete mode 100644 test-suite/bugs/closed/328.v
 delete mode 100644 test-suite/bugs/closed/329.v
 delete mode 100644 test-suite/bugs/closed/331.v
 delete mode 100644 test-suite/bugs/closed/335.v
 delete mode 100644 test-suite/bugs/closed/348.v
 delete mode 100644 test-suite/bugs/closed/38.v
 delete mode 100644 test-suite/bugs/closed/545.v
 create mode 100644 test-suite/bugs/closed/5797.v
 create mode 100644 test-suite/bugs/closed/5845.v
 create mode 100644 test-suite/bugs/closed/5940.v
 delete mode 100644 test-suite/bugs/closed/846.v
 delete mode 100644 test-suite/bugs/closed/931.v
 create mode 100644 test-suite/bugs/opened/1615.v
 delete mode 100644 test-suite/bugs/opened/743.v

diff --git a/test-suite/bugs/closed/1100.v b/test-suite/bugs/closed/1100.v
deleted file mode 100644
index 32c78b4b9e..0000000000
--- a/test-suite/bugs/closed/1100.v
+++ /dev/null
@@ -1,12 +0,0 @@
-Require Import Setoid.
-
-Parameter P : nat -> Prop.
-Parameter Q : nat -> Prop.
-Parameter PQ : forall n, P n <-> Q n.
-
-Lemma PQ2 : forall n, P n -> Q n.
-  intros.
-  rewrite PQ in H.
-  trivial.
-Qed.
-
diff --git a/test-suite/bugs/closed/121.v b/test-suite/bugs/closed/121.v
deleted file mode 100644
index 8c5a38859f..0000000000
--- a/test-suite/bugs/closed/121.v
+++ /dev/null
@@ -1,17 +0,0 @@
-Require Import Setoid.
-
-Section Setoid_Bug.
-
-Variable X:Type -> Type.
-Variable Xeq : forall A, (X A) -> (X A) -> Prop.
-Hypothesis Xst : forall A, Equivalence (Xeq A).
-
-Variable map : forall A B, (A -> B) -> X A -> X B.
-
-Implicit Arguments map [A B].
-
-Goal forall A B (a b:X (B -> A)) (c:X A) (f:A -> B -> A), Xeq _ a b -> Xeq _ b (map f c) -> Xeq _ a (map f c).
-intros A B a b c f Hab Hbc.
-rewrite Hab.
-assumption.
-Qed.
diff --git a/test-suite/bugs/closed/1238.v b/test-suite/bugs/closed/1238.v
new file mode 100644
index 0000000000..6b6e83779f
--- /dev/null
+++ b/test-suite/bugs/closed/1238.v
@@ -0,0 +1,22 @@
+Require Import Setoid.
+
+Variable A : Set.
+
+Inductive liste : Set :=
+| vide : liste
+| c : A -> liste -> liste.
+
+Inductive e : A -> liste -> Prop :=
+| ec : forall (x : A) (l : liste), e x (c x l)
+| ee : forall (x y : A) (l : liste), e x l -> e x (c y l).
+
+Definition same := fun (l m : liste) => forall (x : A), e x l <-> e x m.
+
+Definition same_refl (x:liste) : (same x x).
+  unfold same; split; intros; trivial.
+Qed.
+
+Goal forall (x:liste), (same x x).
+  intro.
+  apply (same_refl x).
+Qed.
diff --git a/test-suite/bugs/closed/1341.v b/test-suite/bugs/closed/1341.v
new file mode 100644
index 0000000000..8c5a38859f
--- /dev/null
+++ b/test-suite/bugs/closed/1341.v
@@ -0,0 +1,17 @@
+Require Import Setoid.
+
+Section Setoid_Bug.
+
+Variable X:Type -> Type.
+Variable Xeq : forall A, (X A) -> (X A) -> Prop.
+Hypothesis Xst : forall A, Equivalence (Xeq A).
+
+Variable map : forall A B, (A -> B) -> X A -> X B.
+
+Implicit Arguments map [A B].
+
+Goal forall A B (a b:X (B -> A)) (c:X A) (f:A -> B -> A), Xeq _ a b -> Xeq _ b (map f c) -> Xeq _ a (map f c).
+intros A B a b c f Hab Hbc.
+rewrite Hab.
+assumption.
+Qed.
diff --git a/test-suite/bugs/closed/1362.v b/test-suite/bugs/closed/1362.v
new file mode 100644
index 0000000000..6cafb9f0cd
--- /dev/null
+++ b/test-suite/bugs/closed/1362.v
@@ -0,0 +1,26 @@
+(** Omega is now aware of the bodies of context variables
+    (of type Z or nat). *)
+
+Require Import ZArith Omega.
+Open Scope Z.
+
+Goal let x := 3 in x = 3.
+intros.
+omega.
+Qed.
+
+Open Scope nat.
+
+Goal let x := 2 in x = 2.
+intros.
+omega.
+Qed.
+
+(** NB: this could be disabled for compatibility reasons *)
+
+Unset Omega UseLocalDefs.
+
+Goal let x := 4 in x = 4.
+intros.
+Fail omega.
+Abort.
diff --git a/test-suite/bugs/closed/148.v b/test-suite/bugs/closed/148.v
deleted file mode 100644
index 6cafb9f0cd..0000000000
--- a/test-suite/bugs/closed/148.v
+++ /dev/null
@@ -1,26 +0,0 @@
-(** Omega is now aware of the bodies of context variables
-    (of type Z or nat). *)
-
-Require Import ZArith Omega.
-Open Scope Z.
-
-Goal let x := 3 in x = 3.
-intros.
-omega.
-Qed.
-
-Open Scope nat.
-
-Goal let x := 2 in x = 2.
-intros.
-omega.
-Qed.
-
-(** NB: this could be disabled for compatibility reasons *)
-
-Unset Omega UseLocalDefs.
-
-Goal let x := 4 in x = 4.
-intros.
-Fail omega.
-Abort.
diff --git a/test-suite/bugs/closed/1542.v b/test-suite/bugs/closed/1542.v
new file mode 100644
index 0000000000..52cfbbc496
--- /dev/null
+++ b/test-suite/bugs/closed/1542.v
@@ -0,0 +1,40 @@
+Module Type TITI.
+Parameter B:Set.
+Parameter x:B.
+Inductive A:Set:=
+a1:B->A.
+Definition f2: A ->B
+:= fun (a:A) =>
+match a with
+ (a1 b)=>b
+end.
+Definition f: A -> B:=fun (a:A) => x.
+End TITI.
+
+
+Module Type TIT.
+Declare Module t:TITI.
+End TIT.
+
+Module Seq(titi:TIT).
+Module t:=titi.t.
+Inductive toto:t.A->t.B->Set:=
+t1:forall (a:t.A), (toto a (t.f a))
+| t2:forall (a:t.A), (toto a (t.f2 a)).
+End Seq.
+
+Module koko(tit:TIT).
+Module seq:=Seq tit.
+Module t':=tit.t.
+
+Definition def:forall (a:t'.A), (seq.toto a (t'.f a)).
+intro ; constructor 1.
+Defined.
+
+Definition def2: forall (a:t'.A), (seq.toto a (t'.f2 a)).
+intro; constructor 2.
+(*  Toplevel input, characters 0-13
+  constructor 2.
+  ^^^^^^^^^^^^^
+Error: Impossible to unify (seq.toto ?3 (seq.t.f2 ?3)) with
+ (seq.toto a (t'.f2 a)).*)
diff --git a/test-suite/bugs/closed/1543.v b/test-suite/bugs/closed/1543.v
new file mode 100644
index 0000000000..def6ed98dd
--- /dev/null
+++ b/test-suite/bugs/closed/1543.v
@@ -0,0 +1,100 @@
+Module Sylvain_Boulme.
+Module Type Essai.
+Parameter T: Type.
+Parameter my_eq: T -> T -> Prop.
+Parameter my_eq_refl: forall (x:T), (my_eq x x).
+Parameter c: T.
+End Essai.
+
+Module Type Essai2.
+Declare Module M: Essai.
+Parameter c2: M.T.
+End Essai2.
+
+Module Type Essai3.
+Declare Module M: Essai.
+Parameter c3: M.T.
+End Essai3.
+
+Module Type Lift.
+Declare Module Core: Essai.
+Declare Module M: Essai.
+Parameter lift: Core.T -> M.T.
+Parameter lift_prop:forall (x:Core.T), (Core.my_eq x Core.c)->(M.my_eq (lift x) M.c).
+End Lift.
+
+Module I2 (X:Essai) <: Essai2.
+ Module Core := X.
+ Module M<:Essai.
+  Definition T:Type :=Prop.
+  Definition my_eq:=(@eq Prop).
+  Definition c:=True.
+  Lemma my_eq_refl: forall (x:T), (my_eq x x).
+  Proof.
+    unfold my_eq; auto.
+  Qed.
+ End M.
+ Definition c2:=False.
+ Definition lift:=fun (_:Core.T) => M.c.
+ Definition lift_prop: forall (x:Core.T), (Core.my_eq x Core.c)->(M.my_eq (lift x) M.c).
+ Proof.
+   unfold lift, M.my_eq; auto.
+ Qed.
+End I2.
+
+Module I4(X:Essai3) (L: Lift with Module Core := X.M) <: Essai3 with Module
+M:=L.M.
+  Module M:=L.M.
+  Definition c3:=(L.lift X.c3).
+End I4.
+
+Module I5(X:Essai3).
+  Module Toto<:  Lift with Module Core := X.M := I2(X.M).
+  Module E4<: Essai3 with Module M:=Toto.M := I4(X)(Toto).
+(*
+Le typage de E4 echoue avec le message
+ Error: Signature components for label my_eq_refl do not match
+ *)
+
+  Module E3<: Essai3 := I4(X)(Toto).
+
+ Definition zarb: forall (x:Toto.M.T), (Toto.M.my_eq x x) := E3.M.my_eq_refl.
+End I5.
+End Sylvain_Boulme.
+
+
+Module Jacek.
+
+    Module Type SIG.
+    End SIG.
+    Module N.
+      Definition A:=Set.
+    End N.
+    Module Type SIG2.
+      Declare Module M:SIG.
+      Parameter B:Type.
+    End SIG2.
+    Module F(X:SIG2 with Module M:=N) (Y:SIG2 with Definition B:=X.M.A).
+    End F.
+End Jacek.
+
+
+Module anoun.
+    Module Type TITI.
+    Parameter X: Set.
+    End TITI.
+
+    Module Type Ex.
+    Declare Module t: TITI.
+    Parameter X : t.X -> t.X -> Set.
+    End Ex.
+
+    Module unionEx(X1: Ex) (X2:Ex with Module t :=X1.t): Ex.
+    Module t:=X1.t.
+    Definition X :=fun (a b:t.X) => ((X1.X a b)+(X2.X a b))%type.
+    End unionEx.
+End anoun.
+(* Le warning qui s'affiche lors de la compilation est le suivant :
+    TODO:replace module after with!
+    Est ce qu'il y'a qq1 qui pourrait m'aider à comprendre le probleme?!
+    Je vous remercie d'avance *)
diff --git a/test-suite/bugs/closed/1545.v b/test-suite/bugs/closed/1545.v
new file mode 100644
index 0000000000..9ef796faf7
--- /dev/null
+++ b/test-suite/bugs/closed/1545.v
@@ -0,0 +1,20 @@
+Module Type TIT.
+
+Inductive X:Set:=
+ b:X.
+End TIT.
+
+
+Module Type TOTO.
+Declare Module t:TIT.
+Inductive titi:Set:=
+ a:t.X->titi.
+End TOTO.
+
+
+Module toto (ta:TOTO).
+Module ti:=ta.t.
+
+Definition ex1:forall (c d:ti.X), (ta.a d)=(ta.a c) -> d=c.
+intros.
+injection H.
diff --git a/test-suite/bugs/closed/1547.v b/test-suite/bugs/closed/1547.v
new file mode 100644
index 0000000000..166fa7a9f2
--- /dev/null
+++ b/test-suite/bugs/closed/1547.v
@@ -0,0 +1,5 @@
+(* Compatibility of Require with backtracking at interactive module end *)
+
+Module A.
+Require List.
+End A.
diff --git a/test-suite/bugs/closed/1551.v b/test-suite/bugs/closed/1551.v
new file mode 100644
index 0000000000..48f0b55129
--- /dev/null
+++ b/test-suite/bugs/closed/1551.v
@@ -0,0 +1,13 @@
+Module Type S.
+  Parameter empty: Set.
+End S.
+
+Module D (M:S).
+  Import M.
+  Definition empty:=nat.
+End D.
+
+Module D' (M:S).
+  Import M.
+  Definition empty:Set. exact nat. Qed.
+End D'.
diff --git a/test-suite/bugs/closed/1584.v b/test-suite/bugs/closed/1584.v
new file mode 100644
index 0000000000..926af7dd1c
--- /dev/null
+++ b/test-suite/bugs/closed/1584.v
@@ -0,0 +1,5 @@
+Require Export Reals.
+
+Parameter toto : nat -> nat -> nat.
+
+Notation " e # f " := (toto e f) (at level 30, f at level 0).
diff --git a/test-suite/bugs/closed/328.v b/test-suite/bugs/closed/328.v
deleted file mode 100644
index 52cfbbc496..0000000000
--- a/test-suite/bugs/closed/328.v
+++ /dev/null
@@ -1,40 +0,0 @@
-Module Type TITI.
-Parameter B:Set.
-Parameter x:B.
-Inductive A:Set:=
-a1:B->A.
-Definition f2: A ->B
-:= fun (a:A) =>
-match a with
- (a1 b)=>b
-end.
-Definition f: A -> B:=fun (a:A) => x.
-End TITI.
-
-
-Module Type TIT.
-Declare Module t:TITI.
-End TIT.
-
-Module Seq(titi:TIT).
-Module t:=titi.t.
-Inductive toto:t.A->t.B->Set:=
-t1:forall (a:t.A), (toto a (t.f a))
-| t2:forall (a:t.A), (toto a (t.f2 a)).
-End Seq.
-
-Module koko(tit:TIT).
-Module seq:=Seq tit.
-Module t':=tit.t.
-
-Definition def:forall (a:t'.A), (seq.toto a (t'.f a)).
-intro ; constructor 1.
-Defined.
-
-Definition def2: forall (a:t'.A), (seq.toto a (t'.f2 a)).
-intro; constructor 2.
-(*  Toplevel input, characters 0-13
-  constructor 2.
-  ^^^^^^^^^^^^^
-Error: Impossible to unify (seq.toto ?3 (seq.t.f2 ?3)) with
- (seq.toto a (t'.f2 a)).*)
diff --git a/test-suite/bugs/closed/329.v b/test-suite/bugs/closed/329.v
deleted file mode 100644
index def6ed98dd..0000000000
--- a/test-suite/bugs/closed/329.v
+++ /dev/null
@@ -1,100 +0,0 @@
-Module Sylvain_Boulme.
-Module Type Essai.
-Parameter T: Type.
-Parameter my_eq: T -> T -> Prop.
-Parameter my_eq_refl: forall (x:T), (my_eq x x).
-Parameter c: T.
-End Essai.
-
-Module Type Essai2.
-Declare Module M: Essai.
-Parameter c2: M.T.
-End Essai2.
-
-Module Type Essai3.
-Declare Module M: Essai.
-Parameter c3: M.T.
-End Essai3.
-
-Module Type Lift.
-Declare Module Core: Essai.
-Declare Module M: Essai.
-Parameter lift: Core.T -> M.T.
-Parameter lift_prop:forall (x:Core.T), (Core.my_eq x Core.c)->(M.my_eq (lift x) M.c).
-End Lift.
-
-Module I2 (X:Essai) <: Essai2.
- Module Core := X.
- Module M<:Essai.
-  Definition T:Type :=Prop.
-  Definition my_eq:=(@eq Prop).
-  Definition c:=True.
-  Lemma my_eq_refl: forall (x:T), (my_eq x x).
-  Proof.
-    unfold my_eq; auto.
-  Qed.
- End M.
- Definition c2:=False.
- Definition lift:=fun (_:Core.T) => M.c.
- Definition lift_prop: forall (x:Core.T), (Core.my_eq x Core.c)->(M.my_eq (lift x) M.c).
- Proof.
-   unfold lift, M.my_eq; auto.
- Qed.
-End I2.
-
-Module I4(X:Essai3) (L: Lift with Module Core := X.M) <: Essai3 with Module
-M:=L.M.
-  Module M:=L.M.
-  Definition c3:=(L.lift X.c3).
-End I4.
-
-Module I5(X:Essai3).
-  Module Toto<:  Lift with Module Core := X.M := I2(X.M).
-  Module E4<: Essai3 with Module M:=Toto.M := I4(X)(Toto).
-(*
-Le typage de E4 echoue avec le message
- Error: Signature components for label my_eq_refl do not match
- *)
-
-  Module E3<: Essai3 := I4(X)(Toto).
-
- Definition zarb: forall (x:Toto.M.T), (Toto.M.my_eq x x) := E3.M.my_eq_refl.
-End I5.
-End Sylvain_Boulme.
-
-
-Module Jacek.
-
-    Module Type SIG.
-    End SIG.
-    Module N.
-      Definition A:=Set.
-    End N.
-    Module Type SIG2.
-      Declare Module M:SIG.
-      Parameter B:Type.
-    End SIG2.
-    Module F(X:SIG2 with Module M:=N) (Y:SIG2 with Definition B:=X.M.A).
-    End F.
-End Jacek.
-
-
-Module anoun.
-    Module Type TITI.
-    Parameter X: Set.
-    End TITI.
-
-    Module Type Ex.
-    Declare Module t: TITI.
-    Parameter X : t.X -> t.X -> Set.
-    End Ex.
-
-    Module unionEx(X1: Ex) (X2:Ex with Module t :=X1.t): Ex.
-    Module t:=X1.t.
-    Definition X :=fun (a b:t.X) => ((X1.X a b)+(X2.X a b))%type.
-    End unionEx.
-End anoun.
-(* Le warning qui s'affiche lors de la compilation est le suivant :
-    TODO:replace module after with!
-    Est ce qu'il y'a qq1 qui pourrait m'aider à comprendre le probleme?!
-    Je vous remercie d'avance *)
diff --git a/test-suite/bugs/closed/331.v b/test-suite/bugs/closed/331.v
deleted file mode 100644
index 9ef796faf7..0000000000
--- a/test-suite/bugs/closed/331.v
+++ /dev/null
@@ -1,20 +0,0 @@
-Module Type TIT.
-
-Inductive X:Set:=
- b:X.
-End TIT.
-
-
-Module Type TOTO.
-Declare Module t:TIT.
-Inductive titi:Set:=
- a:t.X->titi.
-End TOTO.
-
-
-Module toto (ta:TOTO).
-Module ti:=ta.t.
-
-Definition ex1:forall (c d:ti.X), (ta.a d)=(ta.a c) -> d=c.
-intros.
-injection H.
diff --git a/test-suite/bugs/closed/335.v b/test-suite/bugs/closed/335.v
deleted file mode 100644
index 166fa7a9f2..0000000000
--- a/test-suite/bugs/closed/335.v
+++ /dev/null
@@ -1,5 +0,0 @@
-(* Compatibility of Require with backtracking at interactive module end *)
-
-Module A.
-Require List.
-End A.
diff --git a/test-suite/bugs/closed/348.v b/test-suite/bugs/closed/348.v
deleted file mode 100644
index 48f0b55129..0000000000
--- a/test-suite/bugs/closed/348.v
+++ /dev/null
@@ -1,13 +0,0 @@
-Module Type S.
-  Parameter empty: Set.
-End S.
-
-Module D (M:S).
-  Import M.
-  Definition empty:=nat.
-End D.
-
-Module D' (M:S).
-  Import M.
-  Definition empty:Set. exact nat. Qed.
-End D'.
diff --git a/test-suite/bugs/closed/38.v b/test-suite/bugs/closed/38.v
deleted file mode 100644
index 6b6e83779f..0000000000
--- a/test-suite/bugs/closed/38.v
+++ /dev/null
@@ -1,22 +0,0 @@
-Require Import Setoid.
-
-Variable A : Set.
-
-Inductive liste : Set :=
-| vide : liste
-| c : A -> liste -> liste.
-
-Inductive e : A -> liste -> Prop :=
-| ec : forall (x : A) (l : liste), e x (c x l)
-| ee : forall (x y : A) (l : liste), e x l -> e x (c y l).
-
-Definition same := fun (l m : liste) => forall (x : A), e x l <-> e x m.
-
-Definition same_refl (x:liste) : (same x x).
-  unfold same; split; intros; trivial.
-Qed.
-
-Goal forall (x:liste), (same x x).
-  intro.
-  apply (same_refl x).
-Qed.
diff --git a/test-suite/bugs/closed/545.v b/test-suite/bugs/closed/545.v
deleted file mode 100644
index 926af7dd1c..0000000000
--- a/test-suite/bugs/closed/545.v
+++ /dev/null
@@ -1,5 +0,0 @@
-Require Export Reals.
-
-Parameter toto : nat -> nat -> nat.
-
-Notation " e # f " := (toto e f) (at level 30, f at level 0).
diff --git a/test-suite/bugs/closed/5797.v b/test-suite/bugs/closed/5797.v
new file mode 100644
index 0000000000..ee5ec1fa6a
--- /dev/null
+++ b/test-suite/bugs/closed/5797.v
@@ -0,0 +1,213 @@
+Set Implicit Arguments.
+
+Open Scope type_scope.
+
+Inductive One : Set := inOne: One.
+
+Definition maybe: forall A B:Set,(A -> B) -> One + A -> One + B.
+Proof.
+  intros A B f c.
+  case c.
+  left; assumption.
+  right; apply f; assumption.
+Defined.
+
+Definition id (A:Set)(a:A):=a.
+
+Definition LamF (X: Set -> Set)(A:Set) :Set :=
+  A + (X A)*(X A) + X(One + A).
+
+Definition LamF' (X: Set -> Set)(A:Set) :Set :=
+  LamF X A.
+
+Require Import List.
+Require Import Bool.
+
+Definition index := list bool.
+
+Inductive L (A:Set) : index -> Set :=
+  initL: A -> L A nil
+  | pluslL: forall l:index, One -> L A (false::l)
+  | plusrL: forall l:index, L A l -> L A (false::l)
+  | varL: forall l:index, L A l -> L A (true::l)
+  | appL: forall l:index, L A (true::l) -> L A (true::l) -> L A (true::l)
+  | absL: forall l:index, L A (true::false::l) -> L A (true::l).
+
+Scheme L_rec_simp := Minimality for L Sort Set.
+
+Definition Lam' (A:Set) := L A (true::nil).
+
+Definition aczelapp: forall (l1 l2: index)(A:Set), L (L A l2) l1 -> L A
+  (l1++l2).
+Proof.
+  intros l1 l2 A.
+  generalize l1.
+  clear l1.
+  (* Check (fun i:index => L A (i++l2)). *)
+  apply (L_rec_simp (A:=L A l2) (fun i:index => L A (i++l2))).
+  trivial.
+  intros l o.
+  simpl app.
+  apply pluslL; assumption.
+  intros l _ t.
+  simpl app.
+  apply plusrL; assumption.
+  intros l _ t.
+  simpl app.
+  apply varL; assumption.
+  intros l _ t1 _ t2.
+  simpl app in *|-*.
+  Check 0.
+  apply appL; [exact t1| exact t2].
+  intros l _ t.
+  simpl app in *|-*.
+  Check 0.
+  apply absL; assumption.
+Defined.
+
+Definition monL: forall (l:index)(A:Set)(B:Set), (A->B) -> L A l -> L B l.
+Proof.
+  intros l A B f.
+  intro t.
+  elim t.
+  intro a.
+  exact (initL (f a)).
+  intros i u.
+  exact (pluslL _ _ u).
+  intros i _ r.
+  exact (plusrL r).
+  intros i _ r.
+  exact (varL r).
+  intros i _ r1 _ r2.
+  exact (appL r1 r2).
+  intros i _ r.
+  exact (absL r).
+Defined.
+
+Definition lam': forall (A B:Set), (A -> B) -> Lam' A -> Lam' B.
+Proof.
+  intros A B f t.
+  unfold Lam' in *|-*.
+  Check 0.
+  exact (monL f t).
+Defined.
+
+Definition inLam': forall A:Set, LamF' Lam' A -> Lam' A.
+Proof.
+  intros A [[a|[t1 t2]]|r].
+  unfold Lam'.
+  exact (varL (initL a)).
+  exact (appL t1 t2).
+  unfold Lam' in * |- *.
+  Check 0.
+  apply absL.
+  change (L A ((true::nil) ++ (false::nil))).
+  apply aczelapp.
+  (* Check (fun x:One + A =>  (match (maybe (fun a:A => initL a) x) with
+    | inl u => pluslL _ _ u
+    | inr t' => plusrL t' end)). *)
+  exact (monL (fun x:One + A =>
+    (match (maybe (fun a:A => initL a) x) with
+       | inl u => pluslL _ _ u
+       | inr t' => plusrL t' end)) r).
+Defined.
+
+Section minimal.
+
+Definition sub1 (F G: Set -> Set):= forall A:Set, F A->G A.
+Hypothesis G: Set -> Set.
+Hypothesis step: sub1 (LamF' G) G.
+
+Fixpoint L'(A:Set)(i:index){struct i} : Set :=
+  match i with
+    nil => A
+    | false::l => One + L' A l
+    | true::l => G (L' A l)
+  end.
+
+Definition LinL': forall (A:Set)(i:index), L A i -> L' A i.
+Proof.
+  intros A i t.
+  elim t.
+  intro a.
+  unfold L'.
+  assumption.
+  intros l u.
+  left; assumption.
+  intros l _ r.
+  right; assumption.
+  intros l _ r.
+  apply (step (A:=L' A l)).
+  exact (inl _ (inl _ r)).
+  intros l _ r1 _ r2.
+  apply (step (A:=L' A l)).
+  (* unfold L' in * |- *.
+  Check 0. *)
+  exact (inl _ (inr _ (pair r1 r2))).
+  intros l _ r.
+  apply  (step (A:=L' A l)).
+  exact (inr _ r).
+Defined.
+
+Definition L'inG: forall A: Set, L' A (true::nil) -> G A.
+Proof.
+  intros A t.
+  unfold L' in t.
+  assumption.
+Defined.
+
+Definition Itbasic: sub1 Lam' G.
+Proof.
+  intros A t.
+  apply L'inG.
+  unfold Lam' in t.
+  exact (LinL' t).
+Defined.
+
+End minimal.
+
+Definition recid := Itbasic inLam'.
+
+Definition L'Lam'inL: forall (i:index)(A:Set), L' Lam' A i -> L A i.
+Proof.
+  intros i A t.
+  induction i.
+  unfold L' in t.
+  apply initL.
+  assumption.
+  induction a.
+  simpl L' in t.
+  apply (aczelapp (l1:=true::nil) (l2:=i)).
+  exact (lam' IHi t).
+  simpl L' in t.
+  induction t.
+  exact (pluslL _ _ a).
+  exact (plusrL (IHi b)).
+Defined.
+
+
+Lemma recidgen: forall(A:Set)(i:index)(t:L A i), L'Lam'inL i A (LinL' inLam' t)
+  = t.
+Proof.
+  intros A i t.
+  induction t.
+  trivial.
+  trivial.
+  simpl.
+  rewrite IHt.
+  trivial.
+  simpl L'Lam'inL.
+  rewrite IHt.
+  trivial.
+  simpl L'Lam'inL.
+  simpl L'Lam'inL in IHt1.
+  unfold lam' in IHt1.
+  simpl L'Lam'inL in IHt2.
+  unfold lam' in IHt2.
+
+  (* going on. This fails for the original solution. *)
+  rewrite IHt1.
+  rewrite IHt2.
+  trivial.
+Abort. (* one goal still left *)
+
diff --git a/test-suite/bugs/closed/5845.v b/test-suite/bugs/closed/5845.v
new file mode 100644
index 0000000000..ea3347a851
--- /dev/null
+++ b/test-suite/bugs/closed/5845.v
@@ -0,0 +1,7 @@
+Parameter P : forall n : nat, n=n -> Prop.
+
+Goal Prop.
+  refine (P _ _).
+    instantiate (1:=0).
+  trivial.
+Qed.
diff --git a/test-suite/bugs/closed/5940.v b/test-suite/bugs/closed/5940.v
new file mode 100644
index 0000000000..32c78b4b9e
--- /dev/null
+++ b/test-suite/bugs/closed/5940.v
@@ -0,0 +1,12 @@
+Require Import Setoid.
+
+Parameter P : nat -> Prop.
+Parameter Q : nat -> Prop.
+Parameter PQ : forall n, P n <-> Q n.
+
+Lemma PQ2 : forall n, P n -> Q n.
+  intros.
+  rewrite PQ in H.
+  trivial.
+Qed.
+
diff --git a/test-suite/bugs/closed/846.v b/test-suite/bugs/closed/846.v
deleted file mode 100644
index ee5ec1fa6a..0000000000
--- a/test-suite/bugs/closed/846.v
+++ /dev/null
@@ -1,213 +0,0 @@
-Set Implicit Arguments.
-
-Open Scope type_scope.
-
-Inductive One : Set := inOne: One.
-
-Definition maybe: forall A B:Set,(A -> B) -> One + A -> One + B.
-Proof.
-  intros A B f c.
-  case c.
-  left; assumption.
-  right; apply f; assumption.
-Defined.
-
-Definition id (A:Set)(a:A):=a.
-
-Definition LamF (X: Set -> Set)(A:Set) :Set :=
-  A + (X A)*(X A) + X(One + A).
-
-Definition LamF' (X: Set -> Set)(A:Set) :Set :=
-  LamF X A.
-
-Require Import List.
-Require Import Bool.
-
-Definition index := list bool.
-
-Inductive L (A:Set) : index -> Set :=
-  initL: A -> L A nil
-  | pluslL: forall l:index, One -> L A (false::l)
-  | plusrL: forall l:index, L A l -> L A (false::l)
-  | varL: forall l:index, L A l -> L A (true::l)
-  | appL: forall l:index, L A (true::l) -> L A (true::l) -> L A (true::l)
-  | absL: forall l:index, L A (true::false::l) -> L A (true::l).
-
-Scheme L_rec_simp := Minimality for L Sort Set.
-
-Definition Lam' (A:Set) := L A (true::nil).
-
-Definition aczelapp: forall (l1 l2: index)(A:Set), L (L A l2) l1 -> L A
-  (l1++l2).
-Proof.
-  intros l1 l2 A.
-  generalize l1.
-  clear l1.
-  (* Check (fun i:index => L A (i++l2)). *)
-  apply (L_rec_simp (A:=L A l2) (fun i:index => L A (i++l2))).
-  trivial.
-  intros l o.
-  simpl app.
-  apply pluslL; assumption.
-  intros l _ t.
-  simpl app.
-  apply plusrL; assumption.
-  intros l _ t.
-  simpl app.
-  apply varL; assumption.
-  intros l _ t1 _ t2.
-  simpl app in *|-*.
-  Check 0.
-  apply appL; [exact t1| exact t2].
-  intros l _ t.
-  simpl app in *|-*.
-  Check 0.
-  apply absL; assumption.
-Defined.
-
-Definition monL: forall (l:index)(A:Set)(B:Set), (A->B) -> L A l -> L B l.
-Proof.
-  intros l A B f.
-  intro t.
-  elim t.
-  intro a.
-  exact (initL (f a)).
-  intros i u.
-  exact (pluslL _ _ u).
-  intros i _ r.
-  exact (plusrL r).
-  intros i _ r.
-  exact (varL r).
-  intros i _ r1 _ r2.
-  exact (appL r1 r2).
-  intros i _ r.
-  exact (absL r).
-Defined.
-
-Definition lam': forall (A B:Set), (A -> B) -> Lam' A -> Lam' B.
-Proof.
-  intros A B f t.
-  unfold Lam' in *|-*.
-  Check 0.
-  exact (monL f t).
-Defined.
-
-Definition inLam': forall A:Set, LamF' Lam' A -> Lam' A.
-Proof.
-  intros A [[a|[t1 t2]]|r].
-  unfold Lam'.
-  exact (varL (initL a)).
-  exact (appL t1 t2).
-  unfold Lam' in * |- *.
-  Check 0.
-  apply absL.
-  change (L A ((true::nil) ++ (false::nil))).
-  apply aczelapp.
-  (* Check (fun x:One + A =>  (match (maybe (fun a:A => initL a) x) with
-    | inl u => pluslL _ _ u
-    | inr t' => plusrL t' end)). *)
-  exact (monL (fun x:One + A =>
-    (match (maybe (fun a:A => initL a) x) with
-       | inl u => pluslL _ _ u
-       | inr t' => plusrL t' end)) r).
-Defined.
-
-Section minimal.
-
-Definition sub1 (F G: Set -> Set):= forall A:Set, F A->G A.
-Hypothesis G: Set -> Set.
-Hypothesis step: sub1 (LamF' G) G.
-
-Fixpoint L'(A:Set)(i:index){struct i} : Set :=
-  match i with
-    nil => A
-    | false::l => One + L' A l
-    | true::l => G (L' A l)
-  end.
-
-Definition LinL': forall (A:Set)(i:index), L A i -> L' A i.
-Proof.
-  intros A i t.
-  elim t.
-  intro a.
-  unfold L'.
-  assumption.
-  intros l u.
-  left; assumption.
-  intros l _ r.
-  right; assumption.
-  intros l _ r.
-  apply (step (A:=L' A l)).
-  exact (inl _ (inl _ r)).
-  intros l _ r1 _ r2.
-  apply (step (A:=L' A l)).
-  (* unfold L' in * |- *.
-  Check 0. *)
-  exact (inl _ (inr _ (pair r1 r2))).
-  intros l _ r.
-  apply  (step (A:=L' A l)).
-  exact (inr _ r).
-Defined.
-
-Definition L'inG: forall A: Set, L' A (true::nil) -> G A.
-Proof.
-  intros A t.
-  unfold L' in t.
-  assumption.
-Defined.
-
-Definition Itbasic: sub1 Lam' G.
-Proof.
-  intros A t.
-  apply L'inG.
-  unfold Lam' in t.
-  exact (LinL' t).
-Defined.
-
-End minimal.
-
-Definition recid := Itbasic inLam'.
-
-Definition L'Lam'inL: forall (i:index)(A:Set), L' Lam' A i -> L A i.
-Proof.
-  intros i A t.
-  induction i.
-  unfold L' in t.
-  apply initL.
-  assumption.
-  induction a.
-  simpl L' in t.
-  apply (aczelapp (l1:=true::nil) (l2:=i)).
-  exact (lam' IHi t).
-  simpl L' in t.
-  induction t.
-  exact (pluslL _ _ a).
-  exact (plusrL (IHi b)).
-Defined.
-
-
-Lemma recidgen: forall(A:Set)(i:index)(t:L A i), L'Lam'inL i A (LinL' inLam' t)
-  = t.
-Proof.
-  intros A i t.
-  induction t.
-  trivial.
-  trivial.
-  simpl.
-  rewrite IHt.
-  trivial.
-  simpl L'Lam'inL.
-  rewrite IHt.
-  trivial.
-  simpl L'Lam'inL.
-  simpl L'Lam'inL in IHt1.
-  unfold lam' in IHt1.
-  simpl L'Lam'inL in IHt2.
-  unfold lam' in IHt2.
-
-  (* going on. This fails for the original solution. *)
-  rewrite IHt1.
-  rewrite IHt2.
-  trivial.
-Abort. (* one goal still left *)
-
diff --git a/test-suite/bugs/closed/931.v b/test-suite/bugs/closed/931.v
deleted file mode 100644
index ea3347a851..0000000000
--- a/test-suite/bugs/closed/931.v
+++ /dev/null
@@ -1,7 +0,0 @@
-Parameter P : forall n : nat, n=n -> Prop.
-
-Goal Prop.
-  refine (P _ _).
-    instantiate (1:=0).
-  trivial.
-Qed.
diff --git a/test-suite/bugs/opened/1615.v b/test-suite/bugs/opened/1615.v
new file mode 100644
index 0000000000..2825701410
--- /dev/null
+++ b/test-suite/bugs/opened/1615.v
@@ -0,0 +1,12 @@
+Require Import Omega.
+
+Lemma foo : forall n m : Z, (n >= 0)%Z -> (n * m >= 0)%Z -> (n <= n + n * m)%Z.
+Proof.
+  intros. omega.
+Qed.
+
+Lemma foo' : forall n m : nat, n <=  n + n * m.
+Proof.
+  intros. Fail omega.
+Abort.
+
diff --git a/test-suite/bugs/opened/743.v b/test-suite/bugs/opened/743.v
deleted file mode 100644
index 2825701410..0000000000
--- a/test-suite/bugs/opened/743.v
+++ /dev/null
@@ -1,12 +0,0 @@
-Require Import Omega.
-
-Lemma foo : forall n m : Z, (n >= 0)%Z -> (n * m >= 0)%Z -> (n <= n + n * m)%Z.
-Proof.
-  intros. omega.
-Qed.
-
-Lemma foo' : forall n m : nat, n <=  n + n * m.
-Proof.
-  intros. Fail omega.
-Abort.
-
-- 
cgit v1.2.3