Merge commit 'upstream/8.2.beta3+dfsg'

49 files changed, 1508 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/1519.v b/test-suite/bugs/closed/1519.v
new file mode 100644
index 00000000..98e3e214
--- /dev/null
+++ b/test-suite/bugs/closed/1519.v
@@ -0,0 +1,23 @@
+Section S.
+
+  Variable A:Prop.
+  Variable W:A.
+  
+  Remark T: A -> A.
+    intro Z.
+    rename W into Z_.
+    rename Z into W.
+    rename Z_ into Z.
+    exact Z.
+  Qed.
+
+  (* bug :
+     Error:
+     Unbound reference: In environment
+     A : Prop
+     W : A
+     Z : A
+     The reference 2 is free
+     *)
+
+End S.
diff --git a/test-suite/bugs/closed/1780.v b/test-suite/bugs/closed/1780.v
new file mode 100644
index 00000000..3929fbae
--- /dev/null
+++ b/test-suite/bugs/closed/1780.v
@@ -0,0 +1,12 @@
+
+Definition bug := Eval vm_compute in eq_rect.
+(* bug:
+Error: Illegal application (Type Error): 
+The term "eq" of type "forall A : Type, A -> A -> Prop"
+cannot be applied to the terms
+ "x" : "A"
+ "P" : "A -> Type"
+ "x0" : "A"
+The 1st term has type "A" which should be coercible to 
+"Type".
+*)
diff --git a/test-suite/bugs/closed/1787.v b/test-suite/bugs/closed/1787.v
new file mode 100644
index 00000000..8e1024e6
--- /dev/null
+++ b/test-suite/bugs/closed/1787.v
@@ -0,0 +1,11 @@
+Parameter P : nat -> nat -> Prop.
+Parameter Q : nat -> nat -> Prop.
+Axiom A : forall x x' x'', P x x' -> Q x'' x' -> P x x''.
+
+Goal (P 1 3) -> (Q 1 3) -> (P 1 1).
+intros H H'.
+refine ((fun H1 : P 1 _ => let H2 := (_:Q 1 _) in A _ _ _ H1 H2) _).
+clear.
+Admitted.
+
+
diff --git a/test-suite/bugs/closed/shouldfail/1703.v b/test-suite/bugs/closed/shouldfail/1703.v
new file mode 100644
index 00000000..6b5198cc
--- /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/1041.v b/test-suite/bugs/closed/shouldsucceed/1041.v
new file mode 100644
index 00000000..a5de82e0
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1041.v
@@ -0,0 +1,13 @@
+Goal Prop.
+
+pose (P:=(fun x y :Prop => y)).
+evar (Q: (forall X Y,P X Y -> Prop)) .
+
+instantiate (1:= fun _ => _ ) in (Value of Q).
+instantiate (1:= fun _ => _ ) in (Value of Q).
+instantiate (1:= fun _ => _ ) in (Value of Q).
+
+instantiate (1:=H) in (Value  of Q).
+
+Admitted.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1100.v b/test-suite/bugs/closed/shouldsucceed/1100.v
new file mode 100644
index 00000000..6d619c74
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1100.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/shouldsucceed/121.v b/test-suite/bugs/closed/shouldsucceed/121.v
new file mode 100644
index 00000000..d193aa73
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/121.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 (X A) (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/shouldsucceed/1243.v b/test-suite/bugs/closed/shouldsucceed/1243.v
new file mode 100644
index 00000000..7d6781db
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1243.v
@@ -0,0 +1,12 @@
+Require Import ZArith.
+Require Import Arith.
+Open Scope Z_scope.
+
+Theorem r_ex : (forall x y:nat, x + y = x + y)%nat.
+Admitted.
+
+Theorem r_ex' : forall x y:nat, (x + y = x + y)%nat.
+Admitted.
+
+
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1302.v b/test-suite/bugs/closed/shouldsucceed/1302.v
new file mode 100644
index 00000000..e94dfcfb
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1302.v
@@ -0,0 +1,22 @@
+Module Type T.
+
+Parameter A : Type.
+
+Inductive L : Type :=
+| L0 : L (* without this constructor, it works right *)
+| L1 :  A -> L.
+
+End T.
+
+Axiom Tp : Type.
+
+Module TT : T.
+
+Definition A : Type := Tp.
+
+Inductive L : Type :=
+| L0 : L
+| L1 :  A -> L.
+
+End TT.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1322.v b/test-suite/bugs/closed/shouldsucceed/1322.v
new file mode 100644
index 00000000..7e21aa7c
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1322.v
@@ -0,0 +1,24 @@
+Require Import Setoid.
+
+Section transition_gen.
+
+Variable I : Type.
+Variable I_eq :I -> I -> Prop.
+Variable I_eq_equiv : Setoid_Theory I I_eq.
+
+(* Add Relation I I_eq
+  reflexivity proved by I_eq_equiv.(Seq_refl I I_eq) 
+  symmetry proved by I_eq_equiv.(Seq_sym I I_eq)
+  transitivity proved by I_eq_equiv.(Seq_trans I I_eq)
+as I_eq_relation. *)
+
+Add Setoid I I_eq I_eq_equiv as I_with_eq.
+
+Variable F : I -> Type.
+Variable F_morphism : forall i j, I_eq i j -> F i = F j.
+
+
+Add Morphism F with signature I_eq ==> (@eq _) as F_morphism2.
+Admitted.
+
+End transition_gen.
diff --git a/test-suite/bugs/closed/shouldsucceed/1411.v b/test-suite/bugs/closed/shouldsucceed/1411.v
new file mode 100644
index 00000000..e330d46f
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1411.v
@@ -0,0 +1,35 @@
+Require Import List.
+Require Import Program.
+
+Inductive Tree : Set :=
+| Br : Tree -> Tree -> Tree
+| No : nat -> Tree
+.
+
+(* given a tree, we want to know which lists can
+   be used to navigate exactly to a node *)
+Inductive Exact : Tree -> list bool -> Prop :=
+| exDone  n    :              Exact (No n)   nil
+| exLeft  l r p: Exact l p -> Exact (Br l r) (true::p)
+| exRight l r p: Exact r p -> Exact (Br l r) (false::p)
+.
+
+Definition unreachable A : False -> A.
+intros.
+destruct H.
+Defined.
+
+Program Fixpoint fetch t p (x:Exact t p) {struct t} :=
+   match t, p with
+   | No p' , nil      => p'
+   | No p' , _::_     => unreachable nat _
+   | Br l r, nil      => unreachable nat _ 
+   | Br l r, true::t  => fetch l t _
+   | Br l r, false::t => fetch r t _
+   end.
+
+Next Obligation. inversion x. Qed.
+Next Obligation. inversion x. Qed.
+Next Obligation. inversion x; trivial. Qed.
+Next Obligation. inversion x; trivial. Qed.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1414.v b/test-suite/bugs/closed/shouldsucceed/1414.v
new file mode 100644
index 00000000..d3c00808
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1414.v
@@ -0,0 +1,41 @@
+Require Import ZArith Coq.Program.Wf Coq.Program.Utils.
+
+Parameter data:Set.
+
+Inductive t : Set :=
+  | Leaf : t
+  | Node : t -> data -> t -> Z -> t.
+
+Parameter avl : t -> Prop.
+Parameter bst : t -> Prop. 
+Parameter In : data -> t -> Prop. 
+Parameter cardinal : t -> nat.
+Definition card2 (s:t*t) := let (s1,s2) := s in cardinal s1 + cardinal s2.
+
+Parameter split : data -> t -> t*(bool*t).
+Parameter join : t -> data -> t -> t.
+Parameter add : data -> t -> t.
+
+Program Fixpoint union 
+  (s:t*t)
+  (hb1: bst (fst s))(ha1: avl (fst s))(hb2: bst (snd s))(hb2: avl (snd s)) 
+  { measure card2 s } : 
+  {s' : t | bst s' /\ avl s' /\ forall x, In x s' <-> In x (fst s) \/ In x (snd
+s)} := 
+  match s with 
+    | (Leaf,t2) => t2
+    | (t1,Leaf) => t1
+    | (Node l1 v1 r1 h1, Node l2 v2 r2 h2) =>        
+        if (Z_ge_lt_dec h1 h2) then
+          if (Z_eq_dec h2 1) 
+          then add v2 (fst s)
+          else
+            let (l2', r2') := split v1 (snd s) in
+            join (union (l1,l2') _ _ _ _) v1 (union (r1,snd r2') _ _ _ _)
+        else
+          if (Z_eq_dec h1 1) 
+          then add v1 (snd s) 
+          else
+            let (l1', r1') := split v2 (fst s) in
+            join (union (l1',l2) _ _ _ _) v2 (union (snd r1',r2) _ _ _ _)
+  end. 
diff --git a/test-suite/bugs/closed/shouldsucceed/1419.v b/test-suite/bugs/closed/shouldsucceed/1419.v
new file mode 100644
index 00000000..d021107d
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1419.v
@@ -0,0 +1,8 @@
+Goal True.
+  set(a := 0).
+  set(b := a).
+  unfold a in b.
+  clear a.
+  Eval vm_compute in  b.
+  trivial.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1425.v b/test-suite/bugs/closed/shouldsucceed/1425.v
new file mode 100644
index 00000000..8e26209a
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1425.v
@@ -0,0 +1,19 @@
+Require Import Setoid. 
+
+Parameter recursion : forall A : Set, A -> (nat -> A -> A) -> nat -> A.
+
+Axiom recursion_S :
+  forall (A : Set) (EA : relation A) (a : A) (f : nat -> A -> A) (n : nat),
+    EA (recursion A a f (S n)) (f n (recursion A a f n)).
+
+Goal forall n : nat, recursion nat 0 (fun _ _ => 1) (S n) = 1.
+intro n.
+rewrite recursion_S.
+reflexivity.
+Qed.
+
+Goal forall n : nat, recursion nat 0 (fun _ _ => 1) (S n) = 1.
+intro n.
+setoid_rewrite recursion_S.
+reflexivity.
+Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/1446.v b/test-suite/bugs/closed/shouldsucceed/1446.v
new file mode 100644
index 00000000..d4e7cea8
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1446.v
@@ -0,0 +1,20 @@
+Lemma not_true_eq_false : forall (b:bool), b <> true -> b = false.
+Proof.
+ destruct b;intros;trivial. 
+ elim H. 
+ exact (refl_equal true). 
+Qed.
+
+Section BUG.
+
+ Variable b : bool.
+ Hypothesis H  : b <> true.
+ Hypothesis H0 : b = true.
+ Hypothesis H1 : b <> true.
+
+ Goal False.
+  rewrite (not_true_eq_false _ H) in * |-. 
+  contradiction.
+ Qed.
+
+End BUG.
diff --git a/test-suite/bugs/closed/shouldsucceed/1448.v b/test-suite/bugs/closed/shouldsucceed/1448.v
new file mode 100644
index 00000000..fe3b4c8b
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1448.v
@@ -0,0 +1,28 @@
+Require Import Relations.
+Require Import Setoid.
+Require Import Ring_theory.
+Require Import Ring_base.
+
+
+Variable R : Type.
+Variable Rone Rzero : R.
+Variable Rplus Rmult Rminus : R -> R -> R.
+Variable Rneg : R -> R.
+
+Lemma my_ring_theory : @ring_theory R Rzero Rone Rplus Rmult Rminus Rneg (@eq
+R).
+Admitted.
+
+Variable Req : R -> R -> Prop.
+
+Hypothesis Req_refl : reflexive _ Req.
+Hypothesis Req_sym : symmetric _ Req.
+Hypothesis Req_trans : transitive _ Req.
+
+Add Relation R Req
+  reflexivity proved by Req_refl
+  symmetry proved by Req_sym
+  transitivity proved by Req_trans
+  as Req_rel.
+
+Add Ring my_ring : my_ring_theory (abstract).
diff --git a/test-suite/bugs/closed/shouldsucceed/1477.v b/test-suite/bugs/closed/shouldsucceed/1477.v
new file mode 100644
index 00000000..dfc8c328
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1477.v
@@ -0,0 +1,18 @@
+Inductive I : Set :=
+  | A : nat -> nat -> I
+  | B : nat -> nat -> I.
+
+Definition foo1 (x:I) : nat :=
+  match x with
+    | A a b | B a b => S b
+  end.
+
+Definition foo2 (x:I) : nat :=
+  match x with
+    | A _ b | B b _ => S b
+  end.
+
+Definition foo (x:I) : nat :=
+  match x with
+    | A a b | B b a => S b
+  end.
diff --git a/test-suite/bugs/closed/shouldsucceed/1483.v b/test-suite/bugs/closed/shouldsucceed/1483.v
new file mode 100644
index 00000000..a3d7f168
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1483.v
@@ -0,0 +1,10 @@
+Require Import BinPos.
+
+Definition P := (fun x : positive => x = xH).
+
+Goal forall (p q : positive), P q -> q = p -> P p.
+intros; congruence.
+Qed.
+
+
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1507.v b/test-suite/bugs/closed/shouldsucceed/1507.v
new file mode 100644
index 00000000..b484c7dc
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1507.v
@@ -0,0 +1,121 @@
+(*
+   Implementing reals a la Stolzenberg
+
+   Danko Ilik, March 2007
+   svn revision: $Id: 1507.v 10068 2007-08-10 12:06:59Z notin $
+
+   XField.v -- (unfinished) axiomatisation of the theories of real and
+               rational intervals.
+*)
+
+Definition associative (A:Type)(op:A->A->A) := 
+  forall x y z:A, op (op x y) z = op x (op y z).
+
+Definition commutative (A:Type)(op:A->A->A) := 
+  forall x y:A, op x y = op y x.
+
+Definition trichotomous (A:Type)(R:A->A->Prop) :=
+  forall x y:A, R x y \/ x=y \/ R y x.
+
+Definition relation (A:Type) := A -> A -> Prop.
+Definition reflexive (A:Type)(R:relation A) := forall x:A, R x x.
+Definition transitive (A:Type)(R:relation A) := 
+  forall x y z:A, R x y -> R y z -> R x z.
+Definition symmetric (A:Type)(R:relation A) := forall x y:A, R x y -> R y x.
+
+Record interval (X:Set)(le:X->X->Prop) : Set :=
+  interval_make {
+    interval_left : X;
+    interval_right : X;
+    interval_nonempty : le interval_left interval_right
+  }.
+
+Record I (grnd:Set)(le:grnd->grnd->Prop) : Type := Imake {
+  Icar    := interval grnd le;
+  Iplus   : Icar -> Icar -> Icar;
+  Imult   : Icar -> Icar -> Icar;
+  Izero   : Icar;
+  Ione    : Icar;
+  Iopp    : Icar -> Icar;
+  Iinv    : Icar -> Icar;
+  Ic      : Icar -> Icar -> Prop; (* consistency *)
+  (* monoids *)
+  Iplus_assoc    : associative Icar Iplus;
+  Imult_assoc    : associative Icar Imult;
+  (* abelian groups *)
+  Iplus_comm     : commutative Icar Iplus;
+  Imult_comm     : commutative Icar Imult;
+  Iplus_0_l      : forall x:Icar, Ic (Iplus Izero x) x;
+  Iplus_0_r      : forall x:Icar, Ic (Iplus x Izero) x;
+  Imult_0_l      : forall x:Icar, Ic (Imult Ione x) x;
+  Imult_0_r      : forall x:Icar, Ic (Imult x Ione) x;
+  Iplus_opp_r    : forall x:Icar, Ic (Iplus x (Iopp x)) (Izero);
+  Imult_inv_r    : forall x:Icar, ~(Ic x Izero) -> Ic (Imult x (Iinv x)) Ione;
+  (* distributive laws *)
+  Imult_plus_distr_l : forall x x' y y' z z' z'', 
+    Ic x x' -> Ic y y' -> Ic z z' -> Ic z z'' ->
+    Ic (Imult (Iplus x y) z) (Iplus (Imult x' z') (Imult y' z''));
+  (* order and lattice structure *)
+  Ilt          : Icar -> Icar -> Prop;
+  Ilc          := fun (x y:Icar) => Ilt x y \/ Ic x y;
+  Isup         : Icar -> Icar -> Icar;
+  Iinf         : Icar -> Icar -> Icar;
+  Ilt_trans    : transitive _ lt;
+  Ilt_trich    : forall x y:Icar, Ilt x y \/ Ic x y \/ Ilt y x;
+  Isup_lub     : forall x y z:Icar, Ilc x z -> Ilc y z -> Ilc (Isup x y) z;
+  Iinf_glb     : forall x y z:Icar, Ilc x y -> Ilc x z -> Ilc x (Iinf y z);
+  (* order preserves operations? *)
+  (* properties of Ic *)
+  Ic_refl   : reflexive _ Ic;
+  Ic_sym    : symmetric _ Ic
+}.
+
+Definition interval_set (X:Set)(le:X->X->Prop) := 
+  (interval X le) -> Prop. (* can be Set as well *)
+Check interval_set.
+Check Ic.
+Definition consistent (X:Set)(le:X->X->Prop)(TI:I X le)(p:interval_set X le) :=
+  forall I J:interval X le, p I -> p J -> (Ic X le TI) I J.
+Check consistent.
+(* define 'fine' *)
+
+Record N (grnd:Set)(le:grnd->grnd->Prop)(grndI:I grnd le) : Type := Nmake {
+  Ncar    := interval_set grnd le;
+  Nplus   : Ncar -> Ncar -> Ncar;
+  Nmult   : Ncar -> Ncar -> Ncar;
+  Nzero   : Ncar;
+  None    : Ncar;
+  Nopp    : Ncar -> Ncar;
+  Ninv    : Ncar -> Ncar;
+  Nc      : Ncar -> Ncar -> Prop; (* Ncistency *)
+  (* monoids *)
+  Nplus_assoc    : associative Ncar Nplus;
+  Nmult_assoc    : associative Ncar Nmult;
+  (* abelian groups *)
+  Nplus_comm     : commutative Ncar Nplus;
+  Nmult_comm     : commutative Ncar Nmult;
+  Nplus_0_l      : forall x:Ncar, Nc (Nplus Nzero x) x;
+  Nplus_0_r      : forall x:Ncar, Nc (Nplus x Nzero) x;
+  Nmult_0_l      : forall x:Ncar, Nc (Nmult None x) x;
+  Nmult_0_r      : forall x:Ncar, Nc (Nmult x None) x;
+  Nplus_opp_r    : forall x:Ncar, Nc (Nplus x (Nopp x)) (Nzero);
+  Nmult_inv_r    : forall x:Ncar, ~(Nc x Nzero) -> Nc (Nmult x (Ninv x)) None;
+  (* distributive laws *)
+  Nmult_plus_distr_l : forall x x' y y' z z' z'', 
+    Nc x x' -> Nc y y' -> Nc z z' -> Nc z z'' ->
+    Nc (Nmult (Nplus x y) z) (Nplus (Nmult x' z') (Nmult y' z''));
+  (* order and lattice structure *)
+  Nlt          : Ncar -> Ncar -> Prop;
+  Nlc          := fun (x y:Ncar) => Nlt x y \/ Nc x y;
+  Nsup         : Ncar -> Ncar -> Ncar;
+  Ninf         : Ncar -> Ncar -> Ncar;
+  Nlt_trans    : transitive _ lt;
+  Nlt_trich    : forall x y:Ncar, Nlt x y \/ Nc x y \/ Nlt y x;
+  Nsup_lub     : forall x y z:Ncar, Nlc x z -> Nlc y z -> Nlc (Nsup x y) z;
+  Ninf_glb     : forall x y z:Ncar, Nlc x y -> Nlc x z -> Nlc x (Ninf y z);
+  (* order preserves operations? *)
+  (* properties of Nc *)
+  Nc_refl   : reflexive _ Nc;
+  Nc_sym    : symmetric _ Nc
+}.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1519.v b/test-suite/bugs/closed/shouldsucceed/1519.v
new file mode 100644
index 00000000..66bab241
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1519.v
@@ -0,0 +1,14 @@
+Section S.
+
+  Variable A:Prop.
+  Variable W:A.
+
+  Remark T: A -> A.
+    intro Z.
+    rename W into Z_.
+    rename Z into W.
+    rename Z_ into Z.
+    exact Z.
+  Qed.
+
+End S.
diff --git a/test-suite/bugs/closed/shouldsucceed/1568.v b/test-suite/bugs/closed/shouldsucceed/1568.v
new file mode 100644
index 00000000..9f10f749
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1568.v
@@ -0,0 +1,13 @@
+CoInductive A: Set :=
+  mk_A: B -> A
+with B: Set :=
+  mk_B: A -> B.
+
+CoFixpoint a:A := mk_A b 
+with b:B := mk_B a.
+
+Goal b = match a with mk_A a1 => a1 end.
+  simpl. reflexivity.
+Qed.
+
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1576.v b/test-suite/bugs/closed/shouldsucceed/1576.v
new file mode 100644
index 00000000..c9ebbd14
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1576.v
@@ -0,0 +1,38 @@
+Module Type TA.
+Parameter t : Set.
+End TA.
+
+Module Type TB.
+Declare Module A: TA.
+End TB.
+
+Module Type TC.
+Declare Module B : TB.
+End TC.
+
+Module Type TD.
+
+Declare Module B: TB .
+Declare Module C: TC 
+    with Module B := B  . 
+End TD.
+
+Module Type TE.
+Declare Module D : TD.
+End TE.
+
+Module Type TF.
+Declare Module E:  TE.
+End TF.
+
+Module G (D: TD). 
+Module B' := D.C.B.
+End G.
+
+Module H  (F: TF).
+Module I := G(F.E.D).
+End H.
+
+Declare Module F:  TF.
+Module K := H(F).
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1582.v b/test-suite/bugs/closed/shouldsucceed/1582.v
new file mode 100644
index 00000000..47953a66
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1582.v
@@ -0,0 +1,15 @@
+Require Import Peano_dec.
+
+Definition fact_F : 
+  forall (n:nat),
+  (forall m, m<n -> nat) ->
+  nat.
+refine 
+  (fun n fact_rec =>
+     if eq_nat_dec n 0 then 
+        1
+     else
+        let fn := fact_rec (n-1) _ in
+        n * fn).
+Admitted.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1604.v b/test-suite/bugs/closed/shouldsucceed/1604.v
new file mode 100644
index 00000000..22c3df82
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1604.v
@@ -0,0 +1,7 @@
+Require Import Setoid.
+
+Parameter F : nat -> nat.
+Axiom F_id : forall n : nat, n = F n.
+Goal forall n : nat, F n = n.
+intro n. setoid_rewrite F_id at 3. reflexivity.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1614.v b/test-suite/bugs/closed/shouldsucceed/1614.v
new file mode 100644
index 00000000..6bc165d4
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1614.v
@@ -0,0 +1,21 @@
+Require Import Ring.
+Require Import ArithRing.
+
+Fixpoint eq_nat_bool (x y : nat) {struct x} : bool :=
+match x, y with
+| 0, 0 => true
+| S x', S y' => eq_nat_bool x' y'
+| _, _ => false
+end.
+
+Theorem eq_nat_bool_implies_eq : forall x y, eq_nat_bool x y = true -> x = y.
+Proof.
+induction x; destruct y; simpl; intro H; try (reflexivity || inversion H).
+apply IHx in H; rewrite H; reflexivity.
+Qed.
+
+Add Ring MyNatSRing : natSRth (decidable eq_nat_bool_implies_eq).
+
+Goal 0 = 0.
+  ring.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1618.v b/test-suite/bugs/closed/shouldsucceed/1618.v
new file mode 100644
index 00000000..a90290bf
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1618.v
@@ -0,0 +1,23 @@
+Inductive A: Set :=
+| A1: nat -> A.
+
+Definition A_size (a: A) : nat :=
+  match a with
+    | A1 n => 0
+  end.
+
+Require Import Recdef. 
+
+Function n3 (P: A -> Prop) (f: forall n, P (A1 n)) (a: A) {struct a} : P a :=
+  match a  return (P a) with
+    | A1 n => f n
+  end.
+
+
+Function n1 (P: A -> Prop) (f: forall n, P (A1 n)) (a: A) {measure A_size a} :
+P
+a :=
+  match a return (P a) with
+    | A1 n => f n
+  end.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1634.v b/test-suite/bugs/closed/shouldsucceed/1634.v
new file mode 100644
index 00000000..e0c540f3
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1634.v
@@ -0,0 +1,24 @@
+Require Export Relation_Definitions.
+Require Export Setoid.
+
+Variable A : Type.
+Variable S : A -> Type.
+Variable Seq : forall {a:A}, relation (S a).
+
+Hypothesis Seq_refl : forall {a:A} (x : S a), Seq x x.
+Hypothesis Seq_sym : forall {a:A} (x y : S a), Seq x y -> Seq y x.
+Hypothesis Seq_trans : forall {a:A} (x y z : S a), Seq x y -> Seq y z ->
+Seq x z.
+
+Add Parametric Relation a : (S a) Seq
+ reflexivity proved by Seq_refl
+ symmetry proved by Seq_sym
+ transitivity proved by Seq_trans
+ as S_Setoid.
+
+Goal forall (a : A) (x y : S a), Seq x y -> Seq x y.
+  intros a x y H.
+  setoid_replace x with y. 
+  reflexivity.
+  trivial.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1643.v b/test-suite/bugs/closed/shouldsucceed/1643.v
new file mode 100644
index 00000000..4114987d
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1643.v
@@ -0,0 +1,21 @@
+(* 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.
+Admitted.
diff --git a/test-suite/bugs/closed/shouldsucceed/1680.v b/test-suite/bugs/closed/shouldsucceed/1680.v
new file mode 100644
index 00000000..524c7bab
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1680.v
@@ -0,0 +1,9 @@
+Ltac int1 := let h := fresh in intro h.
+
+Goal nat -> nat -> True.
+  let h' := fresh in (let h := fresh in intro h); intro h'.
+  Restart. let h' := fresh in int1; intro h'.
+  trivial.
+Qed.
+
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1683.v b/test-suite/bugs/closed/shouldsucceed/1683.v
new file mode 100644
index 00000000..1571ee20
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1683.v
@@ -0,0 +1,42 @@
+Require Import Setoid.
+
+Section SetoidBug.
+
+Variable ms : Type.
+Variable ms_type : ms -> Type.
+Variable ms_eq : forall (A:ms), relation (ms_type A).
+
+Variable CR : ms.
+
+Record Ring : Type :=
+{Ring_type : Type}.
+
+Variable foo : forall (A:Ring), nat -> Ring_type A.
+Variable IR : Ring.
+Variable IRasCR : Ring_type IR -> ms_type CR.
+
+Definition CRasCRing : Ring := Build_Ring (ms_type CR).
+
+Hypothesis ms_refl : forall A x, ms_eq A x x.
+Hypothesis ms_sym : forall A x y, ms_eq A x y -> ms_eq A y x.
+Hypothesis ms_trans : forall A x y z, ms_eq A x y -> ms_eq A y z -> ms_eq A x z.
+
+Add Parametric Relation A : (ms_type A) (ms_eq A)
+  reflexivity proved by (ms_refl A)
+  symmetry proved by (ms_sym A)
+  transitivity proved by (ms_trans A)
+  as ms_Setoid.
+
+Hypothesis foobar : forall n, ms_eq CR (IRasCR (foo IR n)) (foo CRasCRing n).
+
+Goal forall (b:ms_type CR),
+ ms_eq CR (IRasCR (foo IR O)) b -> 
+ ms_eq CR (IRasCR (foo IR O)) b.
+intros b H.
+rewrite foobar.
+rewrite foobar in H.
+assumption.
+Qed.
+
+
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1696.v b/test-suite/bugs/closed/shouldsucceed/1696.v
new file mode 100644
index 00000000..0826428a
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1696.v
@@ -0,0 +1,16 @@
+Require Import Setoid.
+
+Inductive mynat := z : mynat | s : mynat -> mynat.
+
+Parameter E : mynat -> mynat -> Prop.
+Axiom E_equiv : equiv mynat E.
+
+Add Relation mynat E
+ reflexivity proved by (proj1 E_equiv)
+ symmetry proved by (proj2 (proj2 E_equiv))
+ transitivity proved by (proj1 (proj2 E_equiv))
+as E_rel.
+
+Notation "x == y" := (E x y) (at level 70).
+
+Goal z == s z -> s z == z. intros H. setoid_rewrite H at 2. reflexivity. Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1704.v b/test-suite/bugs/closed/shouldsucceed/1704.v
new file mode 100644
index 00000000..4b02d5f9
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1704.v
@@ -0,0 +1,17 @@
+
+Require Import Setoid.
+Parameter E : nat -> nat -> Prop.
+Axiom E_equiv : equiv nat E.
+Add Relation nat E
+reflexivity proved by (proj1 E_equiv)
+symmetry proved by (proj2 (proj2 E_equiv))
+transitivity proved by (proj1 (proj2 E_equiv))
+as E_rel.
+Notation "x == y" := (E x y) (at level 70, no associativity).
+Axiom r : False -> 0 == 1.
+Goal 0 == 0.
+Proof.
+rewrite r.
+reflexivity.
+admit.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1718.v b/test-suite/bugs/closed/shouldsucceed/1718.v
new file mode 100644
index 00000000..715fa941
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1718.v
@@ -0,0 +1,9 @@
+(* lazy delta unfolding used to miss delta on rels and vars (fixed in 10172) *)
+
+Check
+  let g := fun _ => 0 in
+  fix f (n : nat) :=
+  match n with
+  | 0 => g f
+  | S n' => 0
+  end.
diff --git a/test-suite/bugs/closed/shouldsucceed/1738.v b/test-suite/bugs/closed/shouldsucceed/1738.v
new file mode 100644
index 00000000..0deed366
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1738.v
@@ -0,0 +1,30 @@
+Require Import FSets.
+
+Module SomeSetoids (Import M:FSetInterface.S).
+
+Lemma Equal_refl : forall s, s[=]s.
+Proof. red; split; auto. Qed.
+
+Add Relation t Equal 
+ reflexivity proved by Equal_refl 
+ symmetry proved by eq_sym
+ transitivity proved by eq_trans 
+ as EqualSetoid.
+
+Add Morphism Empty with signature Equal ==> iff as Empty_m.
+Proof.
+unfold Equal, Empty; firstorder.
+Qed.
+
+End SomeSetoids.
+
+Module Test (Import M:FSetInterface.S).
+ Module A:=SomeSetoids M.
+ Module B:=SomeSetoids M. (* lots of warning *)
+
+ Lemma Test : forall s s', s[=]s' -> Empty s -> Empty s'.
+ intros.
+ rewrite H in H0.
+ assumption.
+Qed.
+End Test.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/1740.v b/test-suite/bugs/closed/shouldsucceed/1740.v
new file mode 100644
index 00000000..d9ce546a
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1740.v
@@ -0,0 +1,23 @@
+(* Check that expansion of alias in pattern-matching compilation is no
+   longer dependent of whether the pattern-matching problem occurs in a
+   typed context or at toplevel (solved from revision 10883) *)
+
+Definition f :=
+  fun n m : nat =>
+    match n, m with
+      | O, _ => O
+      | n, O => n
+      | _, _ => O
+    end.
+
+Goal f =
+  fun n m : nat =>
+    match n, m with
+      | O, _ => O
+      | n, O => n
+      | _, _ => O
+    end.
+  unfold f. 
+  reflexivity.
+Qed.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1754.v b/test-suite/bugs/closed/shouldsucceed/1754.v
new file mode 100644
index 00000000..06b8dce8
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1754.v
@@ -0,0 +1,24 @@
+Axiom hp : Set.
+Axiom cont : nat -> hp -> Prop.
+Axiom sconj : (hp -> Prop) -> (hp -> Prop) -> hp -> Prop.
+Axiom sconjImpl : forall h A B,
+  (sconj A B) h -> forall (A' B': hp -> Prop),
+    (forall h', A h' -> A' h') ->
+    (forall h', B h' -> B' h') ->
+    (sconj A' B') h.
+
+Definition cont' (h:hp) := exists y, cont y h.
+
+Lemma foo : forall h x y A,
+  (sconj (cont x) (sconj (cont y) A)) h ->
+  (sconj cont' (sconj cont' A)) h.
+Proof.
+  intros h x y A H.
+  eapply sconjImpl.
+  2:intros h' Hp'; econstructor; apply Hp'.
+  2:intros h' Hp'; eapply sconjImpl.
+  3:intros h'' Hp''; econstructor; apply Hp''.
+  3:intros h'' Hp''; apply Hp''.
+  2:apply Hp'.
+  clear H.
+Admitted.
diff --git a/test-suite/bugs/closed/shouldsucceed/1773.v b/test-suite/bugs/closed/shouldsucceed/1773.v
new file mode 100644
index 00000000..211af89b
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1773.v
@@ -0,0 +1,9 @@
+(* An occur-check test was done too early *)
+
+Goal forall B C : nat -> nat -> Prop, forall k,
+  (exists A, (forall k', C A k' -> B A k') -> B A k).
+Proof.
+  intros B C k.
+  econstructor.
+  intros X.
+  apply X. (* used to fail here *)
diff --git a/test-suite/bugs/closed/shouldsucceed/1774.v b/test-suite/bugs/closed/shouldsucceed/1774.v
new file mode 100644
index 00000000..4c24b481
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1774.v
@@ -0,0 +1,18 @@
+Axiom pl : (nat -> Prop) -> (nat -> Prop) -> (nat -> Prop).
+Axiom plImp : forall k P Q,
+  pl P Q k -> forall (P':nat -> Prop),
+    (forall k', P k' -> P' k') -> forall (Q':nat -> Prop),
+      (forall k', Q k' -> Q' k') ->
+      pl P' Q' k.
+
+Definition nexists (P:nat -> nat -> Prop) : nat -> Prop :=
+  fun k' => exists k, P k k'.
+
+Goal forall k (A:nat -> nat -> Prop) (B:nat -> Prop),
+  pl (nexists A) B k.
+intros.
+eapply plImp.
+2:intros m' M'; econstructor; apply M'.
+2:intros m' M'; apply M'.
+simpl.
+Admitted.
diff --git a/test-suite/bugs/closed/shouldsucceed/1775.v b/test-suite/bugs/closed/shouldsucceed/1775.v
new file mode 100644
index 00000000..dab4120b
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1775.v
@@ -0,0 +1,39 @@
+Axiom pair : nat -> nat -> nat -> Prop.
+Axiom pl : (nat -> Prop) -> (nat -> Prop) -> (nat -> Prop).
+Axiom plImp : forall k P Q,
+  pl P Q k -> forall (P':nat -> Prop),
+    (forall k', P k' -> P' k') -> forall (Q':nat -> Prop),
+      (forall k', Q k' -> Q' k') ->
+      pl P' Q' k.
+
+Definition nexists (P:nat -> nat -> Prop) : nat -> Prop :=
+  fun k' => exists k, P k k'.
+
+Goal forall s k k' m,
+  (pl k' (nexists (fun w => (nexists (fun b => pl (pair w w)
+    (pl (pair s b)
+    (nexists (fun w0 => (nexists (fun a => pl (pair b w0)
+      (nexists (fun w1 => (nexists (fun c => pl 
+        (pair a w1) (pl (pair a c) k))))))))))))))) m.
+intros.
+eapply plImp; [ | eauto | intros ].
+2:econstructor.
+2:econstructor.
+2:eapply plImp; [ | eauto | intros ].
+3:eapply plImp; [ | eauto | intros ].
+4:econstructor.
+4:econstructor.
+4:eapply plImp; [ | eauto | intros ].
+5:econstructor.
+5:econstructor.
+5:eauto.
+4:eauto.
+3:eauto.
+2:eauto.
+
+assert (X := 1).
+clear X.   (* very slow! *)
+
+simpl.  (* exception Not_found *)
+
+Admitted.
diff --git a/test-suite/bugs/closed/shouldsucceed/1776.v b/test-suite/bugs/closed/shouldsucceed/1776.v
new file mode 100644
index 00000000..abf85455
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1776.v
@@ -0,0 +1,22 @@
+Axiom pair : nat -> nat -> nat -> Prop.
+Axiom pl : (nat -> Prop) -> (nat -> Prop) -> (nat -> Prop).
+Axiom plImpR : forall k P Q,
+  pl P Q k -> forall (Q':nat -> Prop),
+    (forall k', Q k' -> Q' k') ->
+    pl P Q' k.
+
+Definition nexists (P:nat -> nat -> Prop) : nat -> Prop :=
+  fun k' => exists k, P k k'.
+
+Goal forall a A m,
+  True ->
+  (pl A (nexists (fun x => (nexists 
+    (fun y => pl (pair a (S x)) (pair a (S y))))))) m.
+Proof.
+  intros.
+  eapply plImpR; [ | intros; econstructor; econstructor; eauto].
+  clear H;
+    match goal with
+       | |- (pl _ (pl (pair _ ?x) _)) _ => replace x with 0
+    end.
+Admitted.
diff --git a/test-suite/bugs/closed/shouldsucceed/1779.v b/test-suite/bugs/closed/shouldsucceed/1779.v
new file mode 100644
index 00000000..95bb66b9
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1779.v
@@ -0,0 +1,25 @@
+Require Import Div2.
+
+Lemma double_div2: forall n, div2 (double n) = n.
+exact (fun n =>  let _subcase :=
+    let _cofact := fun _ : 0 = 0 => refl_equal 0 in
+    _cofact (let _fact := refl_equal 0 in _fact) in
+  let _subcase0 :=
+    fun (m : nat) (Hrec : div2 (double m) = m) =>
+    let _fact := f_equal div2 (double_S m) in
+    let _eq := trans_eq _fact (refl_equal (S (div2 (double m)))) in
+    let _eq0 :=
+      trans_eq _eq
+        (trans_eq
+           (f_equal (fun f : nat -> nat => f (div2 (double m)))
+              (refl_equal S)) (f_equal S Hrec)) in
+    _eq0 in
+  (fix _fix (__ : nat) : div2 (double __) = __ :=
+     match __ as n return (div2 (double n) = n) with
+     | 0 => _subcase
+     | S __0 =>
+         (fun _hrec : div2 (double __0) = __0 => _subcase0 __0 _hrec)
+           (_fix __0)
+     end) n).
+Guarded.
+Defined.
diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v
new file mode 100644
index 00000000..616dd26f
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1784.v
@@ -0,0 +1,101 @@
+Require Import List.
+Require Import ZArith.
+Require String. Open Scope string_scope.
+Ltac Case s := let c := fresh "case" in set (c := s).
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Inductive sv : Set :=
+| I : Z -> sv
+| S : list sv -> sv.
+
+Section sv_induction.
+
+Variables
+  (VP: sv -> Prop)
+  (LP: list sv -> Prop)
+
+  (VPint: forall n, VP (I n))
+  (VPset: forall vs, LP vs -> VP (S vs))
+  (lpcons: forall v vs, VP v -> LP vs -> LP (v::vs))
+  (lpnil: LP nil).
+
+Fixpoint setl_value_indp (x:sv) {struct x}: VP x :=
+  match x as x return VP x with
+  | I n => VPint n
+  | S vs =>
+    VPset
+    ((fix values_indp (vs:list sv) {struct vs}: (LP vs) :=
+      match vs as vs return LP vs with
+      | nil => lpnil
+      | v::vs => lpcons (setl_value_indp v) (values_indp vs)
+      end) vs)
+  end.
+End sv_induction.
+
+Inductive slt : sv -> sv -> Prop :=
+| IC : forall z, slt (I z) (I z)
+| IS : forall vs vs', slist_in vs vs' -> slt (S vs) (S vs')
+
+with sin : sv ->  list sv -> Prop :=
+| Ihd : forall s s' sv', slt s s' -> sin s (s'::sv')
+| Itl : forall s s' sv', sin s sv' -> sin s (s'::sv')
+
+with slist_in : list sv -> list sv -> Prop :=
+| Inil : forall sv',
+  slist_in nil sv'
+| Icons : forall s sv sv',
+  sin s sv' ->
+  slist_in sv sv' ->
+  slist_in (s::sv) sv'.
+
+Hint Constructors sin slt slist_in.
+
+Require Import Program.
+
+Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} :=
+  match x with
+    | I x => 
+      match y with
+        | I y => if (Z_eq_dec x y) then in_left else in_right
+        | S ys => in_right
+      end
+    | S xs => 
+      match y with
+        | I y => in_right
+        | S ys =>
+          let fix list_in (xs ys:list sv) {struct xs} : 
+            {slist_in xs ys} + {~slist_in xs ys} :=
+            match xs with
+              | nil => in_left
+              | x::xs =>
+                let fix elem_in (ys:list sv) : {sin x ys}+{~sin x ys} :=
+                  match ys with
+                    | nil => in_right
+                    | y::ys => if lt_dec x y then in_left else if elem_in
+                      ys then in_left else in_right
+                  end
+                in 
+                if elem_in ys then 
+                  if list_in xs ys then in_left else in_right
+                else in_right
+            end
+            in if list_in xs ys then in_left else in_right
+      end
+  end.
+
+Next Obligation. apply H; inversion H0; subst; trivial. Defined.
+Next Obligation. inversion H. Defined.
+Next Obligation. inversion H. Defined.
+Next Obligation. inversion H; subst. Defined.
+Next Obligation.
+  contradict H. inversion H1; subst. assumption. 
+  contradict H0; assumption. Defined.
+Next Obligation.
+  contradict H0. inversion H1; subst. assumption. Defined.
+Next Obligation.
+  contradict H. inversion H0; subst. assumption. Defined.
+Next Obligation.
+  contradict H. inversion H0; subst; auto. Defined.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1844.v b/test-suite/bugs/closed/shouldsucceed/1844.v
new file mode 100644
index 00000000..545f2615
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1844.v
@@ -0,0 +1,217 @@
+Require Import ZArith.
+
+Definition zeq := Z_eq_dec.
+
+Definition update (A: Set) (x: Z) (v: A) (s: Z -> A) : Z -> A :=
+ fun y => if zeq x y then v else s y.
+
+Implicit Arguments update [A].
+
+Definition ident := Z.
+Parameter operator: Set.
+Parameter value: Set.
+Parameter is_true: value -> Prop.
+Definition label := Z.
+
+Inductive expr : Set :=
+ | Evar: ident -> expr
+ | Econst: value -> expr
+ | Eop: operator -> expr -> expr -> expr.
+
+Inductive stmt : Set :=
+ | Sskip: stmt
+ | Sassign: ident -> expr -> stmt
+ | Scall: ident -> ident -> expr -> stmt (* x := f(e) *)
+ | Sreturn: expr -> stmt
+ | Sseq: stmt -> stmt -> stmt
+ | Sifthenelse: expr -> stmt -> stmt -> stmt
+ | Sloop: stmt -> stmt
+ | Sblock: stmt -> stmt
+ | Sexit: nat -> stmt
+ | Slabel: label -> stmt -> stmt
+ | Sgoto: label -> stmt.
+
+Record function : Set := mkfunction {
+ fn_param: ident;
+ fn_body: stmt
+}.
+
+Parameter program: ident -> option function.
+
+Parameter main_function: ident.
+
+Definition store := ident -> value.
+
+Parameter empty_store : store.
+
+Parameter eval_op: operator -> value -> value -> option value.
+
+Fixpoint eval_expr (st: store) (e: expr) {struct e} : option value :=
+ match e with
+ | Evar v => Some (st v)
+ | Econst v => Some v
+ | Eop op e1 e2 =>
+     match eval_expr st e1, eval_expr st e2 with
+     | Some v1, Some v2 => eval_op op v1 v2
+     | _, _ => None
+     end
+ end.
+
+Inductive outcome: Set :=
+ | Onormal: outcome
+ | Oexit: nat -> outcome
+ | Ogoto: label -> outcome
+ | Oreturn: value -> outcome.
+
+Definition outcome_block (out: outcome) : outcome :=
+ match out with
+ | Onormal => Onormal
+ | Oexit O => Onormal
+ | Oexit (S m) => Oexit m
+ | Ogoto lbl => Ogoto lbl
+ | Oreturn v => Oreturn v
+ end.
+
+Fixpoint label_defined (lbl: label) (s: stmt) {struct s}: Prop :=
+ match s with
+ | Sskip => False
+ | Sassign id e => False
+ | Scall id fn e => False
+ | Sreturn e => False
+ | Sseq s1 s2 => label_defined lbl s1 \/ label_defined lbl s2
+ | Sifthenelse e s1 s2 => label_defined lbl s1 \/ label_defined lbl s2
+ | Sloop s1 => label_defined lbl s1
+ | Sblock s1 => label_defined lbl s1
+ | Sexit n => False
+ | Slabel lbl1 s1 => lbl1 = lbl \/ label_defined lbl s1
+ | Sgoto lbl => False
+ end.
+
+Inductive exec : stmt -> store -> outcome -> store -> Prop :=
+ | exec_skip: forall st,
+     exec Sskip st Onormal st
+ | exec_assign: forall id e st v,
+     eval_expr st e = Some v ->
+     exec (Sassign id e) st Onormal (update id v st)
+ | exec_call: forall id fn e st v1 f v2 st',
+     eval_expr st e = Some v1 ->
+     program fn = Some f ->
+     exec_function f (update f.(fn_param) v1 empty_store) v2 st' ->
+     exec (Scall id fn e) st Onormal (update id v2 st)
+ | exec_return: forall e st v,
+     eval_expr st e = Some v ->
+     exec (Sreturn e) st (Oreturn v) st
+ | exec_seq_2: forall s1 s2 st st1 out' st',
+     exec s1 st Onormal st1 -> exec s2 st1 out' st' ->
+     exec (Sseq s1 s2) st out' st'
+ | exec_seq_1: forall s1 s2 st out st',
+     exec s1 st out st' -> out <> Onormal ->
+     exec (Sseq s1 s2) st out st'
+ | exec_ifthenelse_true: forall e s1 s2 st out st' v,
+     eval_expr st e = Some v -> is_true v -> exec s1 st out st' ->
+     exec (Sifthenelse e s1 s2) st out st'
+ | exec_ifthenelse_false: forall e s1 s2 st out st' v,
+     eval_expr st e = Some v -> ~is_true v -> exec s2 st out st' ->
+     exec (Sifthenelse e s1 s2) st out st'
+ | exec_loop_loop: forall s st st1 out' st',
+     exec s st Onormal st1 ->
+     exec (Sloop s) st1 out' st' ->
+     exec (Sloop s) st out' st'
+ | exec_loop_stop: forall s st st' out,
+     exec s st out st' -> out <> Onormal ->
+     exec (Sloop s) st out st'
+ | exec_block: forall s st out st',
+     exec s st out st' ->
+     exec (Sblock s) st (outcome_block out) st'
+ | exec_exit: forall n st,
+     exec (Sexit n) st (Oexit n) st
+ | exec_label: forall s lbl st st' out,
+     exec s st out st' ->
+     exec (Slabel lbl s) st out st'
+ | exec_goto: forall st lbl,
+     exec (Sgoto lbl) st (Ogoto lbl) st
+
+(** [execg lbl stmt st out st'] starts executing at label [lbl] within [s],
+   in initial store [st].  The result of the execution is the outcome
+   [out] with final store [st']. *)
+
+with execg: label -> stmt -> store -> outcome -> store -> Prop :=
+ | execg_left_seq_2: forall lbl s1 s2 st st1 out' st',
+     execg lbl s1 st Onormal st1 -> exec s2 st1 out' st' ->
+     execg lbl (Sseq s1 s2) st out' st'
+ | execg_left_seq_1: forall lbl s1 s2 st out st',
+     execg lbl s1 st out st' -> out <> Onormal ->
+     execg lbl (Sseq s1 s2) st out st'
+ | execg_right_seq: forall lbl s1 s2 st out st',
+     ~(label_defined lbl s1) ->
+     execg lbl s2 st out st' ->
+     execg lbl (Sseq s1 s2) st out st'
+ | execg_ifthenelse_left: forall lbl e s1 s2 st out st',
+     execg lbl s1 st out st' ->
+     execg lbl (Sifthenelse e s1 s2) st out st'
+ | execg_ifthenelse_right: forall lbl e s1 s2 st out st',
+     ~(label_defined lbl s1) ->
+     execg lbl s2 st out st' ->
+     execg lbl (Sifthenelse e s1 s2) st out st'
+ | execg_loop_loop: forall lbl s st st1 out' st',
+     execg lbl s st Onormal st1 ->
+     exec (Sloop s) st1 out' st' ->
+     execg lbl (Sloop s) st out' st'
+ | execg_loop_stop: forall lbl s st st' out,
+     execg lbl s st out st' -> out <> Onormal ->
+     execg lbl (Sloop s) st out st'
+ | execg_block: forall lbl s st out st',
+     execg lbl s st out st' ->
+     execg lbl (Sblock s) st (outcome_block out) st'
+ | execg_label_found: forall lbl s st st' out,
+     exec s st out st' ->
+     execg lbl (Slabel lbl s) st out st'
+ | execg_label_notfound: forall lbl s lbl' st st' out,
+     lbl' <> lbl ->
+     execg lbl s st out st' ->
+     execg lbl (Slabel lbl' s) st out st'
+
+(** [exec_finish out st st'] takes the outcome [out] and the store [st]
+ at the end of the evaluation of the program.  If [out] is a [goto],
+ execute again the program starting at the corresponding label.
+ Iterate this way until [out] is [Onormal]. *)
+
+with exec_finish: function -> outcome -> store -> value -> store -> Prop :=
+ | exec_finish_normal: forall f st v,
+     exec_finish f (Oreturn v) st v st
+ | exec_finish_goto: forall f lbl st out v st1 st',
+     execg lbl f.(fn_body) st out st1 ->
+     exec_finish f out st1 v st' ->
+     exec_finish f (Ogoto lbl) st v st'
+
+(** Execution of a function *)
+
+with exec_function: function -> store -> value -> store -> Prop :=
+ | exec_function_intro: forall f st out st1 v st',
+     exec f.(fn_body) st out st1 -> 
+     exec_finish f out st1 v st' ->
+     exec_function f st v st'.
+
+Scheme exec_ind4:= Minimality for exec Sort Prop
+ with execg_ind4:= Minimality for execg Sort Prop
+ with exec_finish_ind4 := Minimality for exec_finish Sort Prop
+ with exec_function_ind4 := Minimality for exec_function Sort Prop.
+
+Scheme exec_dind4:= Induction for exec Sort Prop
+ with execg_dind4:= Minimality for execg Sort Prop
+ with exec_finish_dind4 := Induction for exec_finish Sort Prop
+ with exec_function_dind4 := Induction for exec_function Sort Prop.
+
+Combined Scheme exec_inductiond from exec_dind4, execg_dind4, exec_finish_dind4,
+  exec_function_dind4.
+
+Scheme exec_dind4' := Induction for exec Sort Prop
+ with execg_dind4' := Induction for execg Sort Prop
+ with exec_finish_dind4' := Induction for exec_finish Sort Prop
+ with exec_function_dind4' := Induction for exec_function Sort Prop.
+
+Combined Scheme exec_induction from exec_ind4, execg_ind4, exec_finish_ind4,
+  exec_function_ind4.
+
+Combined Scheme exec_inductiond' from exec_dind4', execg_dind4', exec_finish_dind4',
+  exec_function_dind4'.
diff --git a/test-suite/bugs/closed/shouldsucceed/1865.v b/test-suite/bugs/closed/shouldsucceed/1865.v
new file mode 100644
index 00000000..17c19989
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1865.v
@@ -0,0 +1,18 @@
+(* Check that tactics (here dependent inversion) do not generate
+   conversion problems T <= U with sup's of universes in U *)
+
+(* Submitted by David Nowak *)
+
+Inductive list (A:Set) : nat -> Set :=
+| nil : list A O
+| cons : forall n, A -> list A n -> list A (S n).
+
+Definition f (n:nat) : Type :=
+  match n with
+  | O => bool
+  | _ => unit
+  end.
+
+Goal forall A n, list A n -> f n.
+intros A n.
+dependent inversion n.
diff --git a/test-suite/bugs/closed/shouldsucceed/348.v b/test-suite/bugs/closed/shouldsucceed/348.v
new file mode 100644
index 00000000..28cc5cb1
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/348.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. Save.
+End D'.
diff --git a/test-suite/bugs/closed/shouldsucceed/38.v b/test-suite/bugs/closed/shouldsucceed/38.v
new file mode 100644
index 00000000..7bc04b1f
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/38.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.
+Save.
+
+Goal forall (x:liste), (same x x).
+  intro.
+  apply (same_refl x).
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/545.v b/test-suite/bugs/closed/shouldsucceed/545.v
new file mode 100644
index 00000000..926af7dd
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/545.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/shouldsucceed/846.v b/test-suite/bugs/closed/shouldsucceed/846.v
new file mode 100644
index 00000000..a963b225
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/846.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/shouldsucceed/931.v b/test-suite/bugs/closed/shouldsucceed/931.v
new file mode 100644
index 00000000..21f15e72
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/931.v
@@ -0,0 +1,7 @@
+Parameter P : forall n : nat, n=n -> Prop.
+
+Goal Prop.
+  refine (P _ _).
+  instantiate (1:=0).
+  trivial.
+Qed.