summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldsucceed
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /test-suite/bugs/closed/shouldsucceed
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed')
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1041.v13
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1100.v12
-rw-r--r--test-suite/bugs/closed/shouldsucceed/121.v17
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1243.v12
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1302.v22
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1322.v24
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1411.v35
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1414.v41
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1419.v8
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1425.v19
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1446.v20
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1448.v28
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1477.v18
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1483.v10
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1507.v121
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1519.v14
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1568.v13
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1576.v38
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1582.v15
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1604.v7
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1614.v21
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1618.v23
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1634.v24
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1643.v21
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1680.v9
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1683.v42
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1696.v16
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1704.v17
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1718.v9
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1738.v30
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1740.v23
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1754.v24
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1773.v9
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1774.v18
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1775.v39
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1776.v22
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1779.v25
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1784.v101
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1844.v217
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1865.v18
-rw-r--r--test-suite/bugs/closed/shouldsucceed/348.v13
-rw-r--r--test-suite/bugs/closed/shouldsucceed/38.v22
-rw-r--r--test-suite/bugs/closed/shouldsucceed/545.v5
-rw-r--r--test-suite/bugs/closed/shouldsucceed/846.v213
-rw-r--r--test-suite/bugs/closed/shouldsucceed/931.v7
45 files changed, 1455 insertions, 0 deletions
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.