summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed')
-rw-r--r--test-suite/bugs/closed/2105.v2
-rw-r--r--test-suite/bugs/closed/2955.v52
-rw-r--r--test-suite/bugs/closed/shouldfail/2406.v3
-rw-r--r--test-suite/bugs/closed/shouldfail/2586.v5
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1414.v4
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1416.v7
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1507.v1
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1784.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1834.v174
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1844.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1912.v6
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1935.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1962.v55
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2127.v7
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2141.v14
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2181.v3
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2304.v4
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2307.v3
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2320.v14
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2342.v8
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2362.v38
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2378.v608
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2388.v6
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2393.v13
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2404.v46
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2456.v53
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2473.v39
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2603.v33
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2613.v17
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2615.v14
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2616.v7
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2629.v22
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2640.v17
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2668.v6
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2732.v19
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2733.v26
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2734.v15
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2750.v23
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2817.v9
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2836.v39
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2928.v11
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2983.v8
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2995.v9
-rw-r--r--test-suite/bugs/closed/shouldsucceed/3000.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/3004.v7
-rw-r--r--test-suite/bugs/closed/shouldsucceed/3008.v29
46 files changed, 1471 insertions, 13 deletions
diff --git a/test-suite/bugs/closed/2105.v b/test-suite/bugs/closed/2105.v
new file mode 100644
index 00000000..46a416fd
--- /dev/null
+++ b/test-suite/bugs/closed/2105.v
@@ -0,0 +1,2 @@
+
+Definition id (T:Type) := Eval vm_compute in T.
diff --git a/test-suite/bugs/closed/2955.v b/test-suite/bugs/closed/2955.v
new file mode 100644
index 00000000..45e24b5f
--- /dev/null
+++ b/test-suite/bugs/closed/2955.v
@@ -0,0 +1,52 @@
+Require Import Coq.Arith.Arith.
+
+Module A.
+
+ Fixpoint foo (n:nat) :=
+ match n with
+ | 0 => 0
+ | S n => bar n
+ end
+
+ with bar (n:nat) :=
+ match n with
+ | 0 => 0
+ | S n => foo n
+ end.
+
+ Lemma using_foo:
+ forall (n:nat), foo n = 0 /\ bar n = 0.
+ Proof.
+ induction n ; split ; auto ;
+ destruct IHn ; auto.
+ Qed.
+
+End A.
+
+
+Module B.
+
+ Module A := A.
+ Import A.
+
+End B.
+
+Module E.
+
+ Module B := B.
+ Import B.A.
+
+ (* Bug 1 *)
+ Lemma test_1:
+ forall (n:nat), foo n = 0.
+ Proof.
+ intros ; destruct n.
+ reflexivity.
+ specialize (A.using_foo (S n)) ; intros.
+ simpl in H.
+ simpl.
+ destruct H.
+ assumption.
+ Qed.
+
+End E. \ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldfail/2406.v b/test-suite/bugs/closed/shouldfail/2406.v
new file mode 100644
index 00000000..112ea2bb
--- /dev/null
+++ b/test-suite/bugs/closed/shouldfail/2406.v
@@ -0,0 +1,3 @@
+(* Check correct handling of unsupported notations *)
+Notation "'’'" := (fun x => x) (at level 20).
+Definition crash_the_rooster f := ’.
diff --git a/test-suite/bugs/closed/shouldfail/2586.v b/test-suite/bugs/closed/shouldfail/2586.v
new file mode 100644
index 00000000..6111a641
--- /dev/null
+++ b/test-suite/bugs/closed/shouldfail/2586.v
@@ -0,0 +1,5 @@
+Require Import Setoid SetoidClass Program.
+
+Goal forall `(Setoid nat) x y, x == y -> S x == S y.
+ intros.
+ clsubst H0. \ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/1414.v b/test-suite/bugs/closed/shouldsucceed/1414.v
index 495a16bc..ee9e2504 100644
--- a/test-suite/bugs/closed/shouldsucceed/1414.v
+++ b/test-suite/bugs/closed/shouldsucceed/1414.v
@@ -26,13 +26,13 @@ Program Fixpoint union
| 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)
+ if (Z.eq_dec h2 1)
then add v2 s
else
let (l2', r2') := split v1 u in
join (union l1 l2' _ _ _ _) v1 (union r1 (snd r2') _ _ _ _)
else
- if (Z_eq_dec h1 1)
+ if (Z.eq_dec h1 1)
then add v1 s
else
let (l1', r1') := split v2 u in
diff --git a/test-suite/bugs/closed/shouldsucceed/1416.v b/test-suite/bugs/closed/shouldsucceed/1416.v
index da67d9b0..ee092005 100644
--- a/test-suite/bugs/closed/shouldsucceed/1416.v
+++ b/test-suite/bugs/closed/shouldsucceed/1416.v
@@ -1,3 +1,8 @@
+(* In 8.1 autorewrite used to raised an anomaly here *)
+(* After resolution of the bug, autorewrite succeeded *)
+(* From forthcoming 8.4, autorewrite is forbidden to instantiate *)
+(* evars, so the new test just checks it is not an anomaly *)
+
Set Implicit Arguments.
Record Place (Env A: Type) : Type := {
@@ -22,6 +27,4 @@ Lemma autorewrite_raise_anomaly: forall (Env A:Type) (e: Env) (p:Place Env A),
Proof.
intros Env A e p; eapply ex_intro.
autorewrite with placeeq. (* Here is the bug *)
- auto.
-Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1507.v b/test-suite/bugs/closed/shouldsucceed/1507.v
index ea72ba89..f2ab9100 100644
--- a/test-suite/bugs/closed/shouldsucceed/1507.v
+++ b/test-suite/bugs/closed/shouldsucceed/1507.v
@@ -2,7 +2,6 @@
Implementing reals a la Stolzenberg
Danko Ilik, March 2007
- svn revision: $Id: 1507.v 12337 2009-09-17 15:58:14Z glondu $
XField.v -- (unfinished) axiomatisation of the theories of real and
rational intervals.
diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v
index 718b0e86..fb2f0ca9 100644
--- a/test-suite/bugs/closed/shouldsucceed/1784.v
+++ b/test-suite/bugs/closed/shouldsucceed/1784.v
@@ -58,7 +58,7 @@ 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
+ | I y => if (Z.eq_dec x y) then in_left else in_right
| S ys => in_right
end
| S xs =>
diff --git a/test-suite/bugs/closed/shouldsucceed/1834.v b/test-suite/bugs/closed/shouldsucceed/1834.v
new file mode 100644
index 00000000..947d15f0
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1834.v
@@ -0,0 +1,174 @@
+(* This tests rather deep nesting of abstracted terms *)
+
+(* This used to fail before Nov 2011 because of a de Bruijn indice bug
+ in extract_predicate.
+
+ Note: use of eq_ok allows shorten notations but was not in the
+ original example
+*)
+
+Scheme eq_rec_dep := Induction for eq Sort Type.
+
+Section Teq.
+
+Variable P0: Type.
+Variable P1: forall (y0:P0), Type.
+Variable P2: forall y0 (y1:P1 y0), Type.
+Variable P3: forall y0 y1 (y2:P2 y0 y1), Type.
+Variable P4: forall y0 y1 y2 (y3:P3 y0 y1 y2), Type.
+Variable P5: forall y0 y1 y2 y3 (y4:P4 y0 y1 y2 y3), Type.
+
+Variable x0:P0.
+
+Inductive eq0 : P0 -> Prop :=
+ refl0: eq0 x0.
+
+Definition eq_0 y0 := x0 = y0.
+
+Variable x1:P1 x0.
+
+Inductive eq1 : forall y0, P1 y0 -> Prop :=
+ refl1: eq1 x0 x1.
+
+Definition S0_0 y0 (e0:eq_0 y0) :=
+ eq_rec_dep P0 x0 (fun y0 e0 => P1 y0) x1 y0 e0.
+
+Definition eq_ok0 y0 y1 (E: eq_0 y0) := S0_0 y0 E = y1.
+
+Definition eq_1 y0 y1 :=
+ {E0:eq_0 y0 | eq_ok0 y0 y1 E0}.
+
+Variable x2:P2 x0 x1.
+
+Inductive eq2 :
+forall y0 y1, P2 y0 y1 -> Prop :=
+refl2: eq2 x0 x1 x2.
+
+Definition S1_0 y0 (e0:eq_0 y0) :=
+eq_rec_dep P0 x0 (fun y0 e0 => P2 y0 (S0_0 y0 e0)) x2 y0 e0.
+
+Definition S1_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) :=
+ eq_rec_dep (P1 y0) (S0_0 y0 e0) (fun y1 e1 => P2 y0 y1)
+ (S1_0 y0 e0)
+ y1 e1.
+
+Definition eq_ok1 y0 y1 y2 (E: eq_1 y0 y1) :=
+ match E with exist e0 e1 => S1_1 y0 y1 e0 e1 = y2 end.
+
+Definition eq_2 y0 y1 y2 :=
+ {E1:eq_1 y0 y1 | eq_ok1 y0 y1 y2 E1}.
+
+Variable x3:P3 x0 x1 x2.
+
+Inductive eq3 :
+forall y0 y1 y2, P3 y0 y1 y2 -> Prop :=
+refl3: eq3 x0 x1 x2 x3.
+
+Definition S2_0 y0 (e0:eq_0 y0) :=
+eq_rec_dep P0 x0 (fun y0 e0 => P3 y0 (S0_0 y0 e0) (S1_0 y0 e0)) x3 y0 e0.
+
+Definition S2_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) :=
+ eq_rec_dep (P1 y0) (S0_0 y0 e0)
+ (fun y1 e1 => P3 y0 y1 (S1_1 y0 y1 e0 e1))
+ (S2_0 y0 e0)
+ y1 e1.
+
+Definition S2_2 y0 y1 y2 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
+ (e2:S1_1 y0 y1 e0 e1 = y2) :=
+ eq_rec_dep (P2 y0 y1) (S1_1 y0 y1 e0 e1)
+ (fun y2 e2 => P3 y0 y1 y2)
+ (S2_1 y0 y1 e0 e1)
+ y2 e2.
+
+Definition eq_ok2 y0 y1 y2 y3 (E: eq_2 y0 y1 y2) : Prop :=
+ match E with exist (exist e0 e1) e2 =>
+ S2_2 y0 y1 y2 e0 e1 e2 = y3 end.
+
+Definition eq_3 y0 y1 y2 y3 :=
+ {E2: eq_2 y0 y1 y2 | eq_ok2 y0 y1 y2 y3 E2}.
+
+Variable x4:P4 x0 x1 x2 x3.
+
+Inductive eq4 :
+forall y0 y1 y2 y3, P4 y0 y1 y2 y3 -> Prop :=
+refl4: eq4 x0 x1 x2 x3 x4.
+
+Definition S3_0 y0 (e0:eq_0 y0) :=
+eq_rec_dep P0 x0 (fun y0 e0 => P4 y0 (S0_0 y0 e0) (S1_0 y0 e0) (S2_0 y0 e0))
+ x4 y0 e0.
+
+Definition S3_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) :=
+ eq_rec_dep (P1 y0) (S0_0 y0 e0)
+ (fun y1 e1 => P4 y0 y1 (S1_1 y0 y1 e0 e1) (S2_1 y0 y1 e0 e1))
+ (S3_0 y0 e0)
+ y1 e1.
+
+Definition S3_2 y0 y1 y2 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
+ (e2:S1_1 y0 y1 e0 e1 = y2) :=
+ eq_rec_dep (P2 y0 y1) (S1_1 y0 y1 e0 e1)
+ (fun y2 e2 => P4 y0 y1 y2 (S2_2 y0 y1 y2 e0 e1 e2))
+ (S3_1 y0 y1 e0 e1)
+ y2 e2.
+
+Definition S3_3 y0 y1 y2 y3 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
+ (e2:S1_1 y0 y1 e0 e1 = y2) (e3:S2_2 y0 y1 y2 e0 e1 e2 = y3):=
+ eq_rec_dep (P3 y0 y1 y2) (S2_2 y0 y1 y2 e0 e1 e2)
+ (fun y3 e3 => P4 y0 y1 y2 y3)
+ (S3_2 y0 y1 y2 e0 e1 e2)
+ y3 e3.
+
+Definition eq_ok3 y0 y1 y2 y3 y4 (E: eq_3 y0 y1 y2 y3) : Prop :=
+ match E with exist (exist (exist e0 e1) e2) e3 =>
+ S3_3 y0 y1 y2 y3 e0 e1 e2 e3 = y4 end.
+
+Definition eq_4 y0 y1 y2 y3 y4 :=
+ {E3: eq_3 y0 y1 y2 y3 | eq_ok3 y0 y1 y2 y3 y4 E3}.
+
+Variable x5:P5 x0 x1 x2 x3 x4.
+
+Inductive eq5 :
+forall y0 y1 y2 y3 y4, P5 y0 y1 y2 y3 y4 -> Prop :=
+refl5: eq5 x0 x1 x2 x3 x4 x5.
+
+Definition S4_0 y0 (e0:eq_0 y0) :=
+eq_rec_dep P0 x0
+(fun y0 e0 => P5 y0 (S0_0 y0 e0) (S1_0 y0 e0) (S2_0 y0 e0) (S3_0 y0 e0))
+ x5 y0 e0.
+
+Definition S4_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) :=
+ eq_rec_dep (P1 y0) (S0_0 y0 e0)
+ (fun y1 e1 => P5 y0 y1 (S1_1 y0 y1 e0 e1) (S2_1 y0 y1 e0 e1) (S3_1 y0 y1 e0
+e1))
+ (S4_0 y0 e0)
+ y1 e1.
+
+Definition S4_2 y0 y1 y2 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
+ (e2:S1_1 y0 y1 e0 e1 = y2) :=
+ eq_rec_dep (P2 y0 y1) (S1_1 y0 y1 e0 e1)
+ (fun y2 e2 => P5 y0 y1 y2 (S2_2 y0 y1 y2 e0 e1 e2) (S3_2 y0 y1 y2 e0 e1 e2))
+ (S4_1 y0 y1 e0 e1)
+ y2 e2.
+
+Definition S4_3 y0 y1 y2 y3 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
+ (e2:S1_1 y0 y1 e0 e1 = y2) (e3:S2_2 y0 y1 y2 e0 e1 e2 = y3):=
+ eq_rec_dep (P3 y0 y1 y2) (S2_2 y0 y1 y2 e0 e1 e2)
+ (fun y3 e3 => P5 y0 y1 y2 y3 (S3_3 y0 y1 y2 y3 e0 e1 e2 e3))
+ (S4_2 y0 y1 y2 e0 e1 e2)
+ y3 e3.
+
+Definition S4_4 y0 y1 y2 y3 y4 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
+ (e2:S1_1 y0 y1 e0 e1 = y2) (e3:S2_2 y0 y1 y2 e0 e1 e2 = y3)
+ (e4:S3_3 y0 y1 y2 y3 e0 e1 e2 e3 = y4) :=
+ eq_rec_dep (P4 y0 y1 y2 y3) (S3_3 y0 y1 y2 y3 e0 e1 e2 e3)
+ (fun y4 e4 => P5 y0 y1 y2 y3 y4)
+ (S4_3 y0 y1 y2 y3 e0 e1 e2 e3)
+ y4 e4.
+
+Definition eq_ok4 y0 y1 y2 y3 y4 y5 (E: eq_4 y0 y1 y2 y3 y4) : Prop :=
+ match E with exist (exist (exist (exist e0 e1) e2) e3) e4 =>
+ S4_4 y0 y1 y2 y3 y4 e0 e1 e2 e3 e4 = y5 end.
+
+Definition eq_5 y0 y1 y2 y3 y4 y5 :=
+ {E4: eq_4 y0 y1 y2 y3 y4 | eq_ok4 y0 y1 y2 y3 y4 y5 E4 }.
+
+End Teq.
diff --git a/test-suite/bugs/closed/shouldsucceed/1844.v b/test-suite/bugs/closed/shouldsucceed/1844.v
index 5627612f..17eeb352 100644
--- a/test-suite/bugs/closed/shouldsucceed/1844.v
+++ b/test-suite/bugs/closed/shouldsucceed/1844.v
@@ -1,6 +1,6 @@
Require Import ZArith.
-Definition zeq := Z_eq_dec.
+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.
diff --git a/test-suite/bugs/closed/shouldsucceed/1912.v b/test-suite/bugs/closed/shouldsucceed/1912.v
new file mode 100644
index 00000000..987a5417
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1912.v
@@ -0,0 +1,6 @@
+Require Import ZArith.
+
+Goal forall x, Z.succ (Z.pred x) = x.
+intros x.
+omega.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1935.v b/test-suite/bugs/closed/shouldsucceed/1935.v
index 72396d49..d5837619 100644
--- a/test-suite/bugs/closed/shouldsucceed/1935.v
+++ b/test-suite/bugs/closed/shouldsucceed/1935.v
@@ -13,7 +13,7 @@ Qed.
Require Import ZArith.
-Definition f'' (a:bool) := if a then eq (A:= Z) else Zlt.
+Definition f'' (a:bool) := if a then eq (A:= Z) else Z.lt.
Lemma f_refl'' : forall n , f'' true n n.
Proof.
diff --git a/test-suite/bugs/closed/shouldsucceed/1962.v b/test-suite/bugs/closed/shouldsucceed/1962.v
new file mode 100644
index 00000000..a6b0fee5
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1962.v
@@ -0,0 +1,55 @@
+(* Bug 1962.v
+
+Bonjour,
+
+J'ai un exemple de lemme que j'arrivais à prouver avec fsetdec avec la 8.2beta3
+avec la beta4 et la version svn 11447 branche 8.2 çà diverge.
+
+Voici l'exemple en question, l'exmple test2 marche bien dans les deux version,
+test en revanche pose probleme:
+
+*)
+
+Require Export FSets.
+
+(** This module takes a decidable type and
+build finite sets of this type, tactics and defs *)
+
+Module BuildFSets (DecPoints: UsualDecidableType).
+
+Module Export FiniteSetsOfPoints := FSetWeakList.Make DecPoints.
+Module Export FiniteSetsOfPointsProperties :=
+ WProperties FiniteSetsOfPoints.
+Module Export Dec := WDecide FiniteSetsOfPoints.
+Module Export FM := Dec.F.
+
+Definition set_of_points := t.
+Definition Point := DecPoints.t.
+
+Definition couple(x y :Point) : set_of_points :=
+add x (add y empty).
+
+Definition triple(x y t :Point): set_of_points :=
+add x (add y (add t empty)).
+
+Lemma test : forall P A B C A' B' C',
+Equal
+(union (singleton P) (union (triple A B C) (triple A' B' C')))
+(union (triple P B B') (union (couple P A) (triple C A' C'))).
+Proof.
+intros.
+unfold triple, couple.
+Time fsetdec. (* works in 8.2 beta 3, not in beta 4 and final 8.2 *)
+ (* appears to works again in 8.3 and trunk, take 4-6 seconds *)
+Qed.
+
+Lemma test2 : forall A B C,
+Equal
+ (union (singleton C) (couple A B)) (triple A B C).
+Proof.
+intros.
+unfold triple, couple.
+Time fsetdec.
+Qed.
+
+End BuildFSets. \ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2127.v b/test-suite/bugs/closed/shouldsucceed/2127.v
index 20ea4603..142ada26 100644
--- a/test-suite/bugs/closed/shouldsucceed/2127.v
+++ b/test-suite/bugs/closed/shouldsucceed/2127.v
@@ -1,11 +1,8 @@
-(* Check that "apply refl_equal" is not exported as an interactive
+(* Check that "apply eq_refl" is not exported as an interactive
tactic but as a statically globalized one *)
(* (this is a simplification of the original bug report) *)
Module A.
-Hint Rewrite sym_equal using apply refl_equal : foo.
+Hint Rewrite eq_sym using apply eq_refl : foo.
End A.
-
-
-
diff --git a/test-suite/bugs/closed/shouldsucceed/2141.v b/test-suite/bugs/closed/shouldsucceed/2141.v
new file mode 100644
index 00000000..941ae530
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2141.v
@@ -0,0 +1,14 @@
+Require Import FSetList.
+Require Import OrderedTypeEx.
+
+Module NatSet := FSetList.Make (Nat_as_OT).
+Recursive Extraction NatSet.fold.
+
+Module FSetHide (X : FSetInterface.S).
+ Include X.
+End FSetHide.
+
+Module NatSet' := FSetHide NatSet.
+Recursive Extraction NatSet'.fold.
+
+(* Extraction "test2141.ml" NatSet'.fold. *) \ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2181.v b/test-suite/bugs/closed/shouldsucceed/2181.v
new file mode 100644
index 00000000..62820d86
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2181.v
@@ -0,0 +1,3 @@
+Class C.
+Parameter P: C -> Prop.
+Fail Record R: Type := { _: C; u: P _ }.
diff --git a/test-suite/bugs/closed/shouldsucceed/2304.v b/test-suite/bugs/closed/shouldsucceed/2304.v
new file mode 100644
index 00000000..1ac2702b
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2304.v
@@ -0,0 +1,4 @@
+(* This used to fail with an anomaly NotASort at some time *)
+Class A (O: Type): Type := a: O -> Type.
+Fail Goal forall (x: a tt), @a x = @a x.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2307.v b/test-suite/bugs/closed/shouldsucceed/2307.v
new file mode 100644
index 00000000..7c049495
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2307.v
@@ -0,0 +1,3 @@
+Inductive V: nat -> Type := VS n: V (S n).
+Definition f (e: V 1): nat := match e with VS 0 => 3 end.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2320.v b/test-suite/bugs/closed/shouldsucceed/2320.v
new file mode 100644
index 00000000..facb9ecf
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2320.v
@@ -0,0 +1,14 @@
+(* Managing metavariables in the return clause of a match *)
+
+(* This was working in 8.1 but is failing in 8.2 and 8.3. It works in
+ trunk thanks to the new proof engine. It could probably made to work in
+ 8.2 and 8.3 if a return predicate of the form "dummy 0" instead of
+ (or in addition to) a sophisticated predicate of the form
+ "as x in dummy y return match y with 0 => ?P | _ => ID end" *)
+
+Inductive dummy : nat -> Prop := constr : dummy 0.
+
+Lemma failure : forall (x : dummy 0), x = constr.
+Proof.
+intros x.
+refine (match x with constr => _ end).
diff --git a/test-suite/bugs/closed/shouldsucceed/2342.v b/test-suite/bugs/closed/shouldsucceed/2342.v
new file mode 100644
index 00000000..094e5466
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2342.v
@@ -0,0 +1,8 @@
+(* Checking that the type inference algoithme does not commit to an
+ equality over sorts when only a subtyping constraint is around *)
+
+Parameter A : Set.
+Parameter B : A -> Set.
+Parameter F : Set -> Prop.
+Check (F (forall x, B x)).
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2362.v b/test-suite/bugs/closed/shouldsucceed/2362.v
new file mode 100644
index 00000000..febb9c7b
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2362.v
@@ -0,0 +1,38 @@
+Set Implicit Arguments.
+
+Class Pointed (M:Type -> Type) :=
+{
+ creturn: forall {A: Type}, A -> M A
+}.
+
+Unset Implicit Arguments.
+Inductive FPair (A B:Type) (neutral: B) : Type:=
+ fpair : forall (a:A) (b:B), FPair A B neutral.
+Implicit Arguments fpair [[A] [B] [neutral]].
+
+Set Implicit Arguments.
+
+Notation "( x ,> y )" := (fpair x y) (at level 0).
+
+Instance Pointed_FPair B neutral:
+ Pointed (fun A => FPair A B neutral) :=
+ { creturn := fun A (a:A) => (a,> neutral) }.
+Definition blah_fail (x:bool) : FPair bool nat O :=
+ creturn x.
+Set Printing All. Print blah_fail.
+
+Definition blah_explicit (x:bool) : FPair bool nat O :=
+ @creturn _ (Pointed_FPair _ ) _ x.
+
+Print blah_explicit.
+
+
+Instance Pointed_FPair_mono:
+ Pointed (fun A => FPair A nat 0) :=
+ { creturn := fun A (a:A) => (a,> 0) }.
+
+
+Definition blah (x:bool) : FPair bool nat O :=
+ creturn x.
+
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2378.v b/test-suite/bugs/closed/shouldsucceed/2378.v
new file mode 100644
index 00000000..7deec64d
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2378.v
@@ -0,0 +1,608 @@
+(* test with Coq 8.3rc1 *)
+
+Require Import Program.
+
+Inductive Unit: Set := unit: Unit.
+
+Definition eq_dec T := forall x y:T, {x=y}+{x<>y}.
+
+Section TTS_TASM.
+
+Variable Time: Set.
+Variable Zero: Time.
+Variable tle: Time -> Time -> Prop.
+Variable tlt: Time -> Time -> Prop.
+Variable tadd: Time -> Time -> Time.
+Variable tsub: Time -> Time -> Time.
+Variable tmin: Time -> Time -> Time.
+Notation "t1 @<= t2" := (tle t1 t2) (at level 70, no associativity).
+Notation "t1 @< t2" := (tlt t1 t2) (at level 70, no associativity).
+Notation "t1 @+ t2" := (tadd t1 t2) (at level 50, left associativity).
+Notation "t1 @- t2" := (tsub t1 t2) (at level 50, left associativity).
+Notation "t1 @<= t2 @<= t3" := ((tle t1 t2) /\ (tle t2 t3)) (at level 70, t2 at next level).
+Notation "t1 @<= t2 @< t3" := ((tle t1 t2) /\ (tlt t2 t3)) (at level 70, t2 at next level).
+
+Variable tzerop: forall n, (n = Zero) + {Zero @< n}.
+Variable tlt_eq_gt_dec: forall x y, {x @< y} + {x=y} + {y @< x}.
+Variable tle_plus_l: forall n m, n @<= n @+ m.
+Variable tle_lt_eq_dec: forall n m, n @<= m -> {n @< m} + {n = m}.
+
+Variable tzerop_zero: tzerop Zero = inleft (Zero @< Zero) (@eq_refl _ Zero).
+Variable tplus_n_O: forall n, n @+ Zero = n.
+Variable tlt_le_weak: forall n m, n @< m -> n @<= m.
+Variable tlt_irrefl: forall n, ~ n @< n.
+Variable tplus_nlt: forall n m, ~n @+ m @< n.
+Variable tle_n: forall n, n @<= n.
+Variable tplus_lt_compat_l: forall n m p, n @< m -> p @+ n @< p @+ m.
+Variable tlt_trans: forall n m p, n @< m -> m @< p -> n @< p.
+Variable tle_lt_trans: forall n m p, n @<= m -> m @< p -> n @< p.
+Variable tlt_le_trans: forall n m p, n @< m -> m @<= p -> n @< p.
+Variable tle_refl: forall n, n @<= n.
+Variable tplus_le_0: forall n m, n @+ m @<= n -> m = Zero.
+Variable Time_eq_dec: eq_dec Time.
+
+(*************************************************************)
+
+Section PropLogic.
+Variable Predicate: Type.
+
+Inductive LP: Type :=
+ LPPred: Predicate -> LP
+| LPAnd: LP -> LP -> LP
+| LPNot: LP -> LP.
+
+Variable State: Type.
+Variable Sat: State -> Predicate -> Prop.
+
+Fixpoint lpSat st f: Prop :=
+ match f with
+ LPPred p => Sat st p
+ | LPAnd f1 f2 => lpSat st f1 /\ lpSat st f2
+ | LPNot f1 => ~lpSat st f1
+ end.
+End PropLogic.
+
+Implicit Arguments lpSat.
+
+Fixpoint LPTransfo Pred1 Pred2 p2lp (f: LP Pred1): LP Pred2 :=
+ match f with
+ LPPred p => p2lp p
+ | LPAnd f1 f2 => LPAnd _ (LPTransfo Pred1 Pred2 p2lp f1) (LPTransfo Pred1 Pred2 p2lp f2)
+ | LPNot f1 => LPNot _ (LPTransfo Pred1 Pred2 p2lp f1)
+ end.
+Implicit Arguments LPTransfo.
+
+Definition addIndex (Ind:Type) (Pred: Ind -> Type) (i: Ind) f :=
+ LPTransfo (fun p => LPPred _ (existT (fun i => Pred i) i p)) f.
+
+Section TTS.
+
+Variable State: Type.
+
+Record TTS: Type := mkTTS {
+ Init: State -> Prop;
+ Delay: State -> Time -> State -> Prop;
+ Next: State -> State -> Prop;
+ Predicate: Type;
+ Satisfy: State -> Predicate -> Prop
+}.
+
+Definition TTSIndexedProduct Ind (tts: Ind -> TTS): TTS := mkTTS
+ (fun st => forall i, Init (tts i) st)
+ (fun st d st' => forall i, Delay (tts i) st d st')
+ (fun st st' => forall i, Next (tts i) st st')
+ { i: Ind & Predicate (tts i) }
+ (fun st p => Satisfy (tts (projT1 p)) st (projT2 p)).
+
+End TTS.
+
+Section SIMU_F.
+
+Variables StateA StateC: Type.
+
+Record mapping: Type := mkMapping {
+ mState: Type;
+ mInit: StateC -> mState;
+ mNext: mState -> StateC -> mState;
+ mDelay: mState -> StateC -> Time -> mState;
+ mabs: mState -> StateC -> StateA
+}.
+
+Variable m: mapping.
+
+Record simu (Pred: Type) (a: TTS StateA) (c: TTS StateC) (tra: Pred -> LP (Predicate _ a)) (trc: Pred -> LP (Predicate _ c)): Type := simuPrf {
+ inv: (mState m) -> StateC -> Prop;
+ invInit: forall st, Init _ c st -> inv (mInit m st) st;
+ invDelay: forall ex1 st1 st2 d, Delay _ c st1 d st2 -> inv ex1 st1 -> inv (mDelay m ex1 st1 d) st2;
+ invNext: forall ex1 st1 st2, Next _ c st1 st2 -> inv ex1 st1 -> inv (mNext m ex1 st1) st2;
+ simuInit: forall st, Init _ c st -> Init _ a (mabs m (mInit m st) st);
+ simuDelay: forall ex1 st1 st2 d, Delay _ c st1 d st2 -> inv ex1 st1 ->
+ Delay _ a (mabs m ex1 st1) d (mabs m (mDelay m ex1 st1 d) st2);
+ simuNext: forall ex1 st1 st2, Next _ c st1 st2 -> inv ex1 st1 ->
+ Next _ a (mabs m ex1 st1) (mabs m (mNext m ex1 st1) st2);
+ simuPred: forall ext st, inv ext st ->
+ (forall p, lpSat (Satisfy _ c) st (trc p) <-> lpSat (Satisfy _ a) (mabs m ext st) (tra p))
+}.
+
+Theorem satProd: forall State Ind Pred (Sat: forall i, State -> Pred i -> Prop) (st:State) i (f: LP (Pred i)),
+ lpSat (Sat i) st f
+ <->
+ lpSat
+ (fun (st : State) (p : {i : Ind & Pred i}) => Sat (projT1 p) st (projT2 p)) st
+ (addIndex Ind _ i f).
+Proof.
+ induction f; simpl; intros; split; intros; intuition.
+Qed.
+
+Definition trProd (State: Type) Ind (Pred: Ind -> Type) (tts: Ind -> TTS State) (tr: forall i, (Pred i) -> LP (Predicate _ (tts i))):
+ {i:Ind & Pred i} -> LP (Predicate _ (TTSIndexedProduct _ Ind tts)) :=
+ fun p => addIndex Ind _ (projS1 p) (tr (projS1 p) (projS2 p)).
+
+Implicit Arguments trProd.
+Require Import Setoid.
+
+Theorem satTrProd:
+ forall State Ind Pred (tts: Ind -> TTS State)
+ (tr: forall i, (Pred i) -> LP (Predicate _ (tts i))) (st:State) (p: {i:Ind & (Pred i)}),
+ lpSat (Satisfy _ (tts (projS1 p))) st (tr (projS1 p) (projS2 p))
+ <->
+ lpSat (Satisfy _ (TTSIndexedProduct _ _ tts)) st (trProd _ tts tr p).
+Proof.
+ unfold trProd, TTSIndexedProduct; simpl; intros.
+ rewrite (satProd State Ind (fun i => Predicate State (tts i))
+ (fun i => Satisfy _ (tts i))); tauto.
+Qed.
+
+Theorem simuProd:
+ forall Ind (Pred: Ind -> Type) (tta: Ind -> TTS StateA) (ttc: Ind -> TTS StateC)
+ (tra: forall i, (Pred i) -> LP (Predicate _ (tta i)))
+ (trc: forall i, (Pred i) -> LP (Predicate _ (ttc i))),
+ (forall i, simu _ (tta i) (ttc i) (tra i) (trc i)) ->
+ simu _ (TTSIndexedProduct _ Ind tta) (TTSIndexedProduct _ Ind ttc)
+ (trProd Pred tta tra) (trProd Pred ttc trc).
+Proof.
+ intros.
+ apply simuPrf with (fun ex st => forall i, inv _ _ (ttc i) (tra i) (trc i) (X i) ex st); simpl; intros; auto.
+ eapply invInit; eauto.
+ eapply invDelay; eauto.
+ eapply invNext; eauto.
+ eapply simuInit; eauto.
+ eapply simuDelay; eauto.
+ eapply simuNext; eauto.
+ split; simpl; intros.
+ generalize (proj1 (simuPred _ _ _ _ _ (X (projS1 p)) ext st (H (projS1 p)) (projS2 p))); simpl; intro.
+ rewrite <- (satTrProd StateA Ind Pred tta tra); apply H1.
+ rewrite (satTrProd StateC Ind Pred ttc trc); apply H0.
+
+ generalize (proj2 (simuPred _ _ _ _ _ (X (projS1 p)) ext st (H (projS1 p)) (projS2 p))); simpl; intro.
+ rewrite <- (satTrProd StateC Ind Pred ttc trc); apply H1.
+ rewrite (satTrProd StateA Ind Pred tta tra); apply H0.
+Qed.
+
+End SIMU_F.
+
+Section TRANSFO.
+
+Record simu_equiv StateA StateC m1 m2 Pred (a: TTS StateA) (c: TTS StateC) (tra: Pred -> LP (Predicate _ a)) (trc: Pred -> LP (Predicate _ c)): Type := simuEquivPrf {
+ simuLR: simu StateA StateC m1 Pred a c tra trc;
+ simuRL: simu StateC StateA m2 Pred c a trc tra
+}.
+
+Theorem simu_equivProd:
+ forall StateA StateC m1 m2 Ind (Pred: Ind -> Type) (tta: Ind -> TTS StateA) (ttc: Ind -> TTS StateC)
+ (tra: forall i, (Pred i) -> LP (Predicate _ (tta i)))
+ (trc: forall i, (Pred i) -> LP (Predicate _ (ttc i))),
+ (forall i, simu_equiv StateA StateC m1 m2 _ (tta i) (ttc i) (tra i) (trc i)) ->
+ simu_equiv StateA StateC m1 m2 _ (TTSIndexedProduct _ Ind tta) (TTSIndexedProduct _ Ind ttc)
+ (trProd _ _ Pred tta tra) (trProd _ _ Pred ttc trc).
+Proof.
+ intros; split; intros.
+ apply simuProd; intro.
+ elim (X i); auto.
+ apply simuProd; intro.
+ elim (X i); auto.
+Qed.
+
+Record RTLanguage: Type := mkRTLanguage {
+ Syntax: Type;
+ DynamicState: Syntax -> Type;
+ Semantic: forall (mdl:Syntax), TTS (DynamicState mdl);
+ MdlPredicate: Syntax -> Type;
+ MdlPredicateDefinition: forall mdl, MdlPredicate mdl -> LP (Predicate _ (Semantic mdl))
+}.
+
+Record Transformation (l1 l2: RTLanguage): Type := mkTransformation {
+ Tmodel: Syntax l1 -> Syntax l2;
+ Tl1l2: forall mdl, mapping (DynamicState l1 mdl) (DynamicState l2 (Tmodel mdl));
+ Tl2l1: forall mdl, mapping (DynamicState l2 (Tmodel mdl)) (DynamicState l1 mdl);
+ Tpred: forall mdl, MdlPredicate l1 mdl -> LP (MdlPredicate l2 (Tmodel mdl));
+ Tsim: forall mdl, simu_equiv (DynamicState l1 mdl) (DynamicState l2 (Tmodel mdl)) (Tl1l2 mdl) (Tl2l1 mdl)
+ (MdlPredicate l1 mdl) (Semantic l1 mdl) (Semantic l2 (Tmodel mdl))
+ (MdlPredicateDefinition l1 mdl)
+ (fun p => LPTransfo (MdlPredicateDefinition l2 (Tmodel mdl)) (Tpred mdl p))
+}.
+
+Section Product.
+
+Record PSyntax (L: RTLanguage): Type := mkPSyntax {
+ pIndex: Type;
+ pIsEmpty: pIndex + {pIndex -> False};
+ pState: Type;
+ pComponents: pIndex -> Syntax L;
+ pIsShared: forall i, DynamicState L (pComponents i) = pState
+}.
+
+Definition pPredicate (L: RTLanguage) (sys: PSyntax L) := { i : pIndex L sys & MdlPredicate L (pComponents L sys i)}.
+
+(* product with shared state *)
+
+Definition PLanguage (L: RTLanguage): RTLanguage :=
+ mkRTLanguage
+ (PSyntax L)
+ (pState L)
+ (fun mdl => TTSIndexedProduct (pState L mdl) (pIndex L mdl)
+ (fun i => match pIsShared L mdl i in (_ = y) return TTS y with
+ eq_refl => Semantic L (pComponents L mdl i)
+ end))
+ (pPredicate L)
+ (fun mdl => trProd _ _ _ _
+ (fun i pi => match pIsShared L mdl i as e in (_ = y) return
+ (LP (Predicate y
+ match e in (_ = y0) return (TTS y0) with
+ | eq_refl => Semantic L (pComponents L mdl i)
+ end))
+ with
+ | eq_refl => MdlPredicateDefinition L (pComponents L mdl i) pi
+ end)).
+
+Inductive Empty: Type :=.
+
+Record isSharedTransfo l1 l2 tr: Prop := isSharedTransfoPrf {
+sameState: forall mdl i j,
+ DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)) =
+ DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl j));
+sameMState: forall mdl i j,
+ mState _ _ (Tl1l2 _ _ tr (pComponents l1 mdl i)) =
+ mState _ _ (Tl1l2 _ _ tr (pComponents l1 mdl j));
+sameM12: forall mdl i j,
+ Tl1l2 _ _ tr (pComponents l1 mdl i) =
+ match sym_eq (sameState mdl i j) in _=y return mapping _ y with
+ eq_refl => match sym_eq (pIsShared l1 mdl i) in _=x return mapping x _ with
+ eq_refl => match pIsShared l1 mdl j in _=x return mapping x _ with
+ eq_refl => Tl1l2 _ _ tr (pComponents l1 mdl j)
+ end
+ end
+ end;
+sameM21: forall mdl i j,
+ Tl2l1 l1 l2 tr (pComponents l1 mdl i) =
+ match
+ sym_eq (sameState mdl i j) in (_ = y)
+ return (mapping y (DynamicState l1 (pComponents l1 mdl i)))
+ with eq_refl =>
+ match
+ sym_eq (pIsShared l1 mdl i) in (_ = y)
+ return
+ (mapping (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl j))) y)
+ with
+ | eq_refl =>
+ match
+ pIsShared l1 mdl j in (_ = y)
+ return
+ (mapping
+ (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl j))) y)
+ with
+ | eq_refl => Tl2l1 l1 l2 tr (pComponents l1 mdl j)
+ end
+ end
+end
+}.
+
+Definition PTransfoSyntax l1 l2 tr (h: isSharedTransfo l1 l2 tr) mdl :=
+ mkPSyntax l2 (pIndex l1 mdl)
+ (pIsEmpty l1 mdl)
+ (match pIsEmpty l1 mdl return Type with
+ inleft i => DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))
+ |inright h => pState l1 mdl
+ end)
+ (fun i => Tmodel l1 l2 tr (pComponents l1 mdl i))
+ (fun i => match pIsEmpty l1 mdl as y return
+ (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)) =
+ match y with
+ | inleft i0 =>
+ DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i0))
+ | inright _ => pState l1 mdl
+ end)
+ with
+ inleft j => sameState l1 l2 tr h mdl i j
+ | inright h => match h i with end
+ end).
+
+Definition compSemantic l mdl i :=
+ match pIsShared l mdl i in (_=y) return TTS y with
+ eq_refl => Semantic l (pComponents l mdl i)
+ end.
+
+Definition compSemanticEq l mdl i s (e: DynamicState l (pComponents l mdl i) = s) :=
+ match e in (_=y) return TTS y with
+ eq_refl => Semantic l (pComponents l mdl i)
+ end.
+
+Definition Pmap12 l1 l2 tr (h: isSharedTransfo l1 l2 tr) (mdl : PSyntax l1) :=
+match
+ pIsEmpty l1 mdl as s
+ return
+ (mapping (pState l1 mdl)
+ match s with
+ | inleft i => DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))
+ | inright _ => pState l1 mdl
+ end)
+with
+| inleft p =>
+ match
+ pIsShared l1 mdl p in (_ = y)
+ return
+ (mapping y (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl p))))
+ with
+ | eq_refl => Tl1l2 l1 l2 tr (pComponents l1 mdl p)
+ end
+| inright _ =>
+ mkMapping (pState l1 mdl) (pState l1 mdl) Unit
+ (fun _ : pState l1 mdl => unit)
+ (fun (_ : Unit) (_ : pState l1 mdl) => unit)
+ (fun (_ : Unit) (_ : pState l1 mdl) (_ : Time) => unit)
+ (fun (_ : Unit) (X : pState l1 mdl) => X)
+end.
+
+Definition Pmap21 l1 l2 tr (h : isSharedTransfo l1 l2 tr) mdl :=
+match
+ pIsEmpty l1 mdl as s
+ return
+ (mapping
+ match s with
+ | inleft i => DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))
+ | inright _ => pState l1 mdl
+ end (pState l1 mdl))
+with
+| inleft p =>
+ match
+ pIsShared l1 mdl p in (_ = y)
+ return
+ (mapping (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl p))) y)
+ with
+ | eq_refl => Tl2l1 l1 l2 tr (pComponents l1 mdl p)
+ end
+| inright _ =>
+ mkMapping (pState l1 mdl) (pState l1 mdl) Unit
+ (fun _ : pState l1 mdl => unit)
+ (fun (_ : Unit) (_ : pState l1 mdl) => unit)
+ (fun (_ : Unit) (_ : pState l1 mdl) (_ : Time) => unit)
+ (fun (_ : Unit) (X : pState l1 mdl) => X)
+end.
+
+Definition PTpred l1 l2 tr (h : isSharedTransfo l1 l2 tr) mdl (pp : pPredicate l1 mdl):
+ LP (MdlPredicate (PLanguage l2) (PTransfoSyntax l1 l2 tr h mdl)) :=
+match pIsEmpty l1 mdl with
+| inleft _ =>
+ let (x, p) := pp in
+ addIndex (pIndex l1 mdl) (fun i => MdlPredicate l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))) x
+ (LPTransfo (Tpred l1 l2 tr (pComponents l1 mdl x))
+ (LPPred (MdlPredicate l1 (pComponents l1 mdl x)) p))
+| inright f => match f (projS1 pp) with end
+end.
+
+Lemma simu_eqA:
+ forall A1 A2 C m P sa sc tta ttc (h: A2=A1),
+ simu A1 C (match h in (_=y) return mapping _ C with eq_refl => m end)
+ P (match h in (_=y) return TTS y with eq_refl => sa end)
+ sc (fun p => match h in (_=y) return LP (Predicate y _) with eq_refl => tta p end)
+ ttc ->
+ simu A2 C m P sa sc tta ttc.
+admit.
+Qed.
+
+Lemma simu_eqC:
+ forall A C1 C2 m P sa sc tta ttc (h: C2=C1),
+ simu A C1 (match h in (_=y) return mapping A _ with eq_refl => m end)
+ P sa (match h in (_=y) return TTS y with eq_refl => sc end)
+ tta (fun p => match h in (_=y) return LP (Predicate y _) with eq_refl => ttc p end)
+ ->
+ simu A C2 m P sa sc tta ttc.
+admit.
+Qed.
+
+Lemma simu_eqA1:
+ forall A1 A2 C m P sa sc tta ttc (h: A1=A2),
+ simu A1 C m
+ P
+ (match (sym_eq h) in (_=y) return TTS y with eq_refl => sa end) sc
+ (fun p => match (sym_eq h) as e in (_=y) return LP (Predicate y (match e in (_=z) return TTS z with eq_refl => sa end)) with eq_refl => tta p end) ttc
+ ->
+ simu A2 C (match h in (_=y) return mapping _ C with eq_refl => m end) P sa sc tta ttc.
+admit.
+Qed.
+
+Lemma simu_eqA2:
+ forall A1 A2 C m P sa sc tta ttc (h: A1=A2),
+ simu A1 C (match (sym_eq h) in (_=y) return mapping _ C with eq_refl => m end)
+ P
+ sa sc tta ttc
+ ->
+ simu A2 C m P
+ (match h in (_=y) return TTS y with eq_refl => sa end) sc
+ (fun p => match h as e in (_=y) return LP (Predicate y match e in (_=y0) return TTS y0 with eq_refl => sa end) with eq_refl => tta p end)
+ ttc.
+admit.
+Qed.
+
+Lemma simu_eqC2:
+ forall A C1 C2 m P sa sc tta ttc (h: C1=C2),
+ simu A C1 (match (sym_eq h) in (_=y) return mapping A _ with eq_refl => m end)
+ P
+ sa sc tta ttc
+ ->
+ simu A C2 m P
+ sa (match h in (_=y) return TTS y with eq_refl => sc end)
+ tta (fun p => match h as e in (_=y) return LP (Predicate y match e in (_=y0) return TTS y0 with eq_refl => sc end) with eq_refl => ttc p end).
+admit.
+Qed.
+
+Lemma simu_eqM:
+ forall A C m1 m2 P sa sc tta ttc (h: m1=m2),
+ simu A C m1 P sa sc tta ttc
+ ->
+ simu A C m2 P sa sc tta ttc.
+admit.
+Qed.
+
+Lemma LPTransfo_trans:
+ forall Pred1 Pred2 Pred3 (tr1: Pred1 -> LP Pred2) (tr2: Pred2 -> LP Pred3) f,
+ LPTransfo tr2 (LPTransfo tr1 f) = LPTransfo (fun x => LPTransfo tr2 (tr1 x)) f.
+Proof.
+ admit.
+Qed.
+
+Lemma LPTransfo_addIndex:
+ forall Ind Pred tr1 x (tr2: forall i, Pred i -> LP (tr1 i)) (p: LP (Pred x)),
+ addIndex Ind tr1 x (LPTransfo (tr2 x) p) =
+ LPTransfo
+ (fun p0 : {i : Ind & Pred i} =>
+ addIndex Ind tr1 (projT1 p0) (tr2 (projT1 p0) (projT2 p0)))
+ (addIndex Ind Pred x p).
+Proof.
+ unfold addIndex; intros.
+ rewrite LPTransfo_trans.
+ rewrite LPTransfo_trans.
+ simpl.
+ auto.
+Qed.
+
+Record tr_compat I0 I1 tr := compatPrf {
+ and_compat: forall p1 p2, tr (LPAnd I0 p1 p2) = LPAnd I1 (tr p1) (tr p2);
+ not_compat: forall p, tr (LPNot I0 p) = LPNot I1 (tr p)
+}.
+
+Lemma LPTransfo_addIndex_tr:
+ forall Ind Pred tr0 tr1 x (tr2: forall i, Pred i -> LP (tr0 i)) (tr3: forall i, LP (tr0 i) -> LP (tr1 i)) (p: LP (Pred x)),
+ (forall x, tr_compat (tr0 x) (tr1 x) (tr3 x)) ->
+ addIndex Ind tr1 x (tr3 x (LPTransfo (tr2 x) p)) =
+ LPTransfo
+ (fun p0 : {i : Ind & Pred i} =>
+ addIndex Ind tr1 (projT1 p0) (tr3 (projT1 p0) (tr2 (projT1 p0) (projT2 p0))))
+ (addIndex Ind Pred x p).
+Proof.
+ unfold addIndex; simpl; intros.
+ rewrite LPTransfo_trans; simpl.
+ rewrite <- LPTransfo_trans.
+ f_equal.
+ induction p; simpl; intros; auto.
+ rewrite (and_compat _ _ _ (H x)).
+ rewrite <- IHp1, <- IHp2; auto.
+ rewrite <- IHp.
+ rewrite (not_compat _ _ _ (H x)); auto.
+Qed.
+
+Require Export Coq.Logic.FunctionalExtensionality.
+Print PLanguage.
+Program Definition PTransfo l1 l2 (tr: Transformation l1 l2) (h: isSharedTransfo l1 l2 tr):
+Transformation (PLanguage l1) (PLanguage l2) :=
+ mkTransformation (PLanguage l1) (PLanguage l2)
+ (PTransfoSyntax l1 l2 tr h)
+ (Pmap12 l1 l2 tr h)
+ (Pmap21 l1 l2 tr h)
+ (PTpred l1 l2 tr h)
+ (fun mdl => simu_equivProd
+ (pState l1 mdl)
+ (pState l2 (PTransfoSyntax l1 l2 tr h mdl))
+ (Pmap12 l1 l2 tr h mdl)
+ (Pmap21 l1 l2 tr h mdl)
+ (pIndex l1 mdl)
+ (fun i => MdlPredicate l1 (pComponents l1 mdl i))
+ (compSemantic l1 mdl)
+ (compSemantic l2 (PTransfoSyntax l1 l2 tr h mdl))
+ _
+ _
+ _
+ ).
+
+Next Obligation.
+ unfold compSemantic, PTransfoSyntax; simpl.
+ case (pIsEmpty l1 mdl); simpl; intros.
+ unfold pPredicate; simpl.
+ unfold pPredicate in X; simpl in X.
+ case (sameState l1 l2 tr h mdl i p).
+ apply (LPTransfo (MdlPredicateDefinition l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)))).
+ apply (LPTransfo (Tpred l1 l2 tr (pComponents l1 mdl i))).
+ apply (LPPred _ X).
+
+ apply False_rect; apply (f i).
+Defined.
+
+Next Obligation.
+ split; intros.
+ unfold Pmap12; simpl.
+ unfold PTransfo_obligation_1; simpl.
+ unfold compSemantic; simpl.
+ unfold eq_ind, eq_rect, f_equal; simpl.
+ case (pIsEmpty l1 mdl); intros.
+ apply simu_eqA2.
+ apply simu_eqC2.
+ apply simu_eqM with (Tl1l2 l1 l2 tr (pComponents l1 mdl i)).
+ apply sameM12.
+ apply (simuLR _ _ _ _ _ _ _ _ _ (Tsim l1 l2 tr (pComponents l1 mdl i))); intro.
+
+ apply False_rect; apply (f i).
+
+ unfold Pmap21; simpl.
+ unfold PTransfo_obligation_1; simpl.
+ unfold compSemantic; simpl.
+ unfold eq_ind, eq_rect, f_equal; simpl.
+ case (pIsEmpty l1 mdl); intros.
+ apply simu_eqC2.
+ apply simu_eqA2.
+ apply simu_eqM with (Tl2l1 l1 l2 tr (pComponents l1 mdl i)).
+ apply sameM21.
+ apply (simuRL _ _ _ _ _ _ _ _ _ (Tsim l1 l2 tr (pComponents l1 mdl i))); intro.
+
+ apply False_rect; apply (f i).
+Qed.
+
+Next Obligation.
+ unfold trProd; simpl.
+ unfold PTransfo_obligation_1; simpl.
+ unfold compSemantic; simpl.
+ unfold eq_ind, eq_rect, f_equal; simpl.
+ apply functional_extensionality; intro.
+ case x; clear x; intros.
+ unfold PTpred; simpl.
+ case (pIsEmpty l1 mdl); simpl; intros.
+ set (tr0 i :=
+ Predicate (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)))
+ (Semantic l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)))).
+ set (tr1 i :=
+ Predicate (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl p)))
+ match sameState l1 l2 tr h mdl i p in (_ = y) return (TTS y) with
+ | eq_refl => Semantic l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))
+ end).
+ set (tr2 x := MdlPredicateDefinition l2 (Tmodel l1 l2 tr (pComponents l1 mdl x))).
+ set (Pred x := MdlPredicate l2 (Tmodel l1 l2 tr (pComponents l1 mdl x))).
+ set (tr3 x f := match
+ sameState l1 l2 tr h mdl x p as e in (_ = y)
+ return
+ (LP
+ (Predicate y
+ match e in (_ = y0) return (TTS y0) with
+ | eq_refl => Semantic l2 (Tmodel l1 l2 tr (pComponents l1 mdl x))
+ end))
+ with
+ | eq_refl => f
+ end).
+ apply (LPTransfo_addIndex_tr _ Pred tr0 tr1 x tr2 tr3
+ (Tpred l1 l2 tr (pComponents l1 mdl x) m)).
+ unfold tr0, tr1, tr3; intros; split; simpl; intros; auto.
+ case (sameState l1 l2 tr h mdl x0 p); auto.
+ case (sameState l1 l2 tr h mdl x0 p); auto.
+
+ apply False_rect; apply (f x).
+Qed.
+
+End Product.
diff --git a/test-suite/bugs/closed/shouldsucceed/2388.v b/test-suite/bugs/closed/shouldsucceed/2388.v
index 8cc43ee6..c7926711 100644
--- a/test-suite/bugs/closed/shouldsucceed/2388.v
+++ b/test-suite/bugs/closed/shouldsucceed/2388.v
@@ -2,3 +2,9 @@
Fail Parameters (A:Prop) (a:A A).
+(* This is a variant (reported as part of bug #2347) *)
+
+Require Import EquivDec.
+Fail Program Instance bool_eq_eqdec : EqDec bool eq :=
+ {equiv_dec x y := (fix aux (x y : bool) {struct x}:= aux _ y) x y}.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2393.v b/test-suite/bugs/closed/shouldsucceed/2393.v
new file mode 100644
index 00000000..fb4f9261
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2393.v
@@ -0,0 +1,13 @@
+Require Import Program.
+
+Inductive T := MkT.
+
+Definition sizeOf (t : T) : nat
+ := match t with
+ | MkT => 1
+ end.
+Variable vect : nat -> Type.
+Program Fixpoint idType (t : T) (n := sizeOf t) (b : vect n) {measure n} : T
+ := match t with
+ | MkT => MkT
+ end.
diff --git a/test-suite/bugs/closed/shouldsucceed/2404.v b/test-suite/bugs/closed/shouldsucceed/2404.v
new file mode 100644
index 00000000..fe8eba54
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2404.v
@@ -0,0 +1,46 @@
+(* Check that dependencies in the indices of the type of the terms to
+ match are taken into account and correctly generalized *)
+
+Require Import Relations.Relation_Definitions.
+Require Import Basics.
+
+Record Base := mkBase
+ {(* Primitives *)
+ World : Set
+ (* Names are real, links are theoretical *)
+ ; Name : World -> Set
+
+ ; wweak : World -> World -> Prop
+
+ ; exportw : forall a b : World, (wweak a b) -> (Name b) -> option (Name a)
+}.
+
+Section Derived.
+ Variable base : Base.
+ Definition bWorld := World base.
+ Definition bName := Name base.
+ Definition bexportw := exportw base.
+ Definition bwweak := wweak base.
+
+ Implicit Arguments bexportw [a b].
+
+Inductive RstarSetProof {I : Type} (T : I -> I -> Type) : I -> I -> Type :=
+ starReflS : forall a, RstarSetProof T a a
+| starTransS : forall i j k, T i j -> (RstarSetProof T j k) -> RstarSetProof T i k.
+
+Implicit Arguments starTransS [I T i j k].
+
+Definition RstarInv {A : Set} (rel : relation A) : A -> A -> Type := (flip (RstarSetProof (flip rel))).
+
+Definition bwweakFlip (b a : bWorld) : Prop := (bwweak a b).
+Definition Rweak : forall a b : bWorld, Type := RstarInv bwweak.
+
+Fixpoint exportRweak {a b} (aRWb : Rweak a b) (y : bName b) : option (bName a) :=
+ match aRWb,y with
+ | starReflS a, y' => Some y'
+ | starTransS i j k jWk jRWi, y' =>
+ match (bexportw jWk y) with
+ | Some x => exportRweak jRWi x
+ | None => None
+ end
+ end.
diff --git a/test-suite/bugs/closed/shouldsucceed/2456.v b/test-suite/bugs/closed/shouldsucceed/2456.v
new file mode 100644
index 00000000..56f046c4
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2456.v
@@ -0,0 +1,53 @@
+
+Require Import Equality.
+
+Parameter Patch : nat -> nat -> Set.
+
+Inductive Catch (from to : nat) : Type
+ := MkCatch : forall (p : Patch from to),
+ Catch from to.
+Implicit Arguments MkCatch [from to].
+
+Inductive CatchCommute5
+ : forall {from mid1 mid2 to : nat},
+ Catch from mid1
+ -> Catch mid1 to
+ -> Catch from mid2
+ -> Catch mid2 to
+ -> Prop
+ := MkCatchCommute5 :
+ forall {from mid1 mid2 to : nat}
+ (p : Patch from mid1)
+ (q : Patch mid1 to)
+ (q' : Patch from mid2)
+ (p' : Patch mid2 to),
+ CatchCommute5 (MkCatch p) (MkCatch q) (MkCatch q') (MkCatch p').
+
+Inductive CatchCommute {from mid1 mid2 to : nat}
+ (p : Catch from mid1)
+ (q : Catch mid1 to)
+ (q' : Catch from mid2)
+ (p' : Catch mid2 to)
+ : Prop
+ := isCatchCommute5 : forall (catchCommuteDetails : CatchCommute5 p q q' p'),
+ CatchCommute p q q' p'.
+Notation "<< p , q >> <~> << q' , p' >>"
+ := (CatchCommute p q q' p')
+ (at level 60, no associativity).
+
+Lemma CatchCommuteUnique2 :
+ forall {from mid mid' to : nat}
+ {p : Catch from mid} {q : Catch mid to}
+ {q' : Catch from mid'} {p' : Catch mid' to}
+ {q'' : Catch from mid'} {p'' : Catch mid' to}
+ (commute1 : <<p, q>> <~> <<q', p'>>)
+ (commute2 : <<p, q>> <~> <<q'', p''>>),
+ (p' = p'') /\ (q' = q'').
+Proof with auto.
+intros.
+set (X := commute2).
+dependent destruction commute1;
+dependent destruction catchCommuteDetails;
+dependent destruction commute2;
+dependent destruction catchCommuteDetails generalizing X.
+Admitted. \ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2473.v b/test-suite/bugs/closed/shouldsucceed/2473.v
new file mode 100644
index 00000000..4c302512
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2473.v
@@ -0,0 +1,39 @@
+
+Require Import Relations Program Setoid Morphisms.
+
+Section S1.
+ Variable R: nat -> relation bool.
+ Instance HR1: forall n, Transitive (R n). Admitted.
+ Instance HR2: forall n, Symmetric (R n). Admitted.
+ Hypothesis H: forall n a, R n (andb a a) a.
+ Goal forall n a b, R n b a.
+ intros.
+ (* rewrite <- H. *) (* Anomaly: Evar ?.. was not declared. Please report. *)
+ (* idem with setoid_rewrite *)
+(* assert (HR2' := HR2 n). *)
+ rewrite <- H. (* ok *)
+ admit.
+ Qed.
+End S1.
+
+Section S2.
+ Variable R: nat -> relation bool.
+ Instance HR: forall n, Equivalence (R n). Admitted.
+ Hypothesis H: forall n a, R n (andb a a) a.
+ Goal forall n a b, R n a b.
+ intros. rewrite <- H. admit.
+ Qed.
+End S2.
+
+(* the parametrised relation is required to get the problem *)
+Section S3.
+ Variable R: relation bool.
+ Instance HR1': Transitive R. Admitted.
+ Instance HR2': Symmetric R. Admitted.
+ Hypothesis H: forall a, R (andb a a) a.
+ Goal forall a b, R b a.
+ intros.
+ rewrite <- H. (* ok *)
+ admit.
+ Qed.
+End S3. \ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2603.v b/test-suite/bugs/closed/shouldsucceed/2603.v
new file mode 100644
index 00000000..371bfdc5
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2603.v
@@ -0,0 +1,33 @@
+(** Namespace of module vs. namescope of definitions/constructors/...
+
+As noticed by A. Appel in bug #2603, module names and definition
+names used to be in the same namespace. But conflict with names
+of constructors (or 2nd mutual inductive...) used to not be checked
+enough, leading to stange situations.
+
+- In 8.3pl3 we introduced checks that forbid uniformly the following
+ situations.
+
+- For 8.4 we finally managed to make module names and other names
+ live in two separate namespace, hence allowing all of the following
+ situations.
+*)
+
+Module Type T.
+End T.
+
+Declare Module K : T.
+
+Module Type L.
+Declare Module E : T.
+End L.
+
+Module M1 : L with Module E:=K.
+Module E := K.
+Inductive t := E. (* Used to be accepted, but End M1 below was failing *)
+End M1.
+
+Module M2 : L with Module E:=K.
+Inductive t := E.
+Module E := K. (* Used to be accepted *)
+End M2. (* Used to be accepted *)
diff --git a/test-suite/bugs/closed/shouldsucceed/2613.v b/test-suite/bugs/closed/shouldsucceed/2613.v
new file mode 100644
index 00000000..4f0470b1
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2613.v
@@ -0,0 +1,17 @@
+(* Check that eq_sym is still pointing to Logic.eq_sym after use of Function *)
+
+Require Import ZArith.
+Require Recdef.
+
+Axiom nat_eq_dec: forall x y : nat, {x=y}+{x<>y}.
+
+Locate eq_sym. (* Constant Coq.Init.Logic.eq_sym *)
+
+Function loop (n: nat) {measure (fun x => x) n} : bool :=
+ if nat_eq_dec n 0 then false else loop (pred n).
+Proof.
+ admit.
+Defined.
+
+Check eq_sym eq_refl : 0=0.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2615.v b/test-suite/bugs/closed/shouldsucceed/2615.v
new file mode 100644
index 00000000..54e1a07c
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2615.v
@@ -0,0 +1,14 @@
+(* This failed with an anomaly in pre-8.4 because of let-in not
+ properly taken into account in the test for unification pattern *)
+
+Inductive foo : forall A, A -> Prop :=
+| foo_intro : forall A x, foo A x.
+Lemma bar A B f : foo (A -> B) f -> forall x : A, foo B (f x).
+Fail induction 1.
+
+(* Whether these examples should succeed with a non-dependent return predicate
+ or fail because there is well-typed return predicate dependent in f
+ is questionable. As of 25 oct 2011, they succeed *)
+refine (fun p => match p with _ => _ end).
+Undo.
+refine (fun p => match p with foo_intro _ _ => _ end).
diff --git a/test-suite/bugs/closed/shouldsucceed/2616.v b/test-suite/bugs/closed/shouldsucceed/2616.v
new file mode 100644
index 00000000..8758e32d
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2616.v
@@ -0,0 +1,7 @@
+(* Testing ill-typed rewrite which used to succeed in 8.3 *)
+Goal
+ forall (N : nat -> Prop) (g : nat -> sig N) (IN : forall a : sig N, a = g 0),
+ N 0 -> False.
+Proof.
+intros.
+Fail rewrite IN in H.
diff --git a/test-suite/bugs/closed/shouldsucceed/2629.v b/test-suite/bugs/closed/shouldsucceed/2629.v
new file mode 100644
index 00000000..759cd3dd
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2629.v
@@ -0,0 +1,22 @@
+Class Join (t: Type) : Type := mkJoin {join: t -> t -> t -> Prop}.
+
+Class sepalg (t: Type) {JOIN: Join t} : Type :=
+ SepAlg {
+ join_eq: forall {x y z z'}, join x y z -> join x y z' -> z = z';
+ join_assoc: forall {a b c d e}, join a b d -> join d c e ->
+ {f : t & join b c f /\ join a f e};
+ join_com: forall {a b c}, join a b c -> join b a c;
+ join_canc: forall {a1 a2 b c}, join a1 b c -> join a2 b c -> a1=a2;
+
+ unit_for : t -> t -> Prop := fun e a => join e a a;
+ join_ex_units: forall a, {e : t & unit_for e a}
+}.
+
+Definition joins {A} `{Join A} (a b : A) : Prop :=
+ exists c, join a b c.
+
+Lemma join_joins {A} `{sepalg A}: forall {a b c},
+ join a b c -> joins a b.
+Proof.
+ firstorder.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/2640.v b/test-suite/bugs/closed/shouldsucceed/2640.v
new file mode 100644
index 00000000..da0cc68a
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2640.v
@@ -0,0 +1,17 @@
+(* Testing consistency of globalization and interpretation in some
+ extreme cases *)
+
+Section sect.
+
+ (* Simplification of the initial example *)
+ Hypothesis Other: True.
+
+ Lemma C2 : True.
+ proof.
+ Fail have True using Other.
+ Abort.
+
+ (* Variant of the same problem *)
+ Lemma C2 : True.
+ Fail clear; Other.
+ Abort.
diff --git a/test-suite/bugs/closed/shouldsucceed/2668.v b/test-suite/bugs/closed/shouldsucceed/2668.v
new file mode 100644
index 00000000..74c8fa34
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2668.v
@@ -0,0 +1,6 @@
+Require Import MSetPositive.
+Require Import MSetProperties.
+
+Module Pos := MSetPositive.PositiveSet.
+Module PPPP := MSetProperties.WPropertiesOn(Pos).
+Print Module PPPP. \ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2732.v b/test-suite/bugs/closed/shouldsucceed/2732.v
new file mode 100644
index 00000000..f22a8ccc
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2732.v
@@ -0,0 +1,19 @@
+(* Check correct behavior of add_primitive_tactic in TACEXTEND *)
+
+(* Added also the case of eauto and congruence *)
+
+Ltac thus H := solve [H].
+
+Lemma test: forall n : nat, n <= n.
+Proof.
+ intro.
+ thus firstorder.
+ Undo.
+ thus eauto.
+Qed.
+
+Lemma test2: false = true -> False.
+Proof.
+ intro.
+ thus congruence.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/2733.v b/test-suite/bugs/closed/shouldsucceed/2733.v
new file mode 100644
index 00000000..fd7bd3bd
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2733.v
@@ -0,0 +1,26 @@
+Definition goodid : forall {A} (x: A), A := fun A x => x.
+Definition wrongid : forall A (x: A), A := fun {A} x => x.
+
+Inductive ty := N | B.
+
+Inductive alt_list : ty -> ty -> Type :=
+ | nil {k} : alt_list k k
+ | Ncons {k} : nat -> alt_list B k -> alt_list N k
+ | Bcons {k} : bool -> alt_list N k -> alt_list B k.
+
+Definition trullynul k {k'} (l : alt_list k k') :=
+match k,l with
+ |N,l' => Ncons 0 (Bcons true l')
+ |B,l' => Bcons true (Ncons 0 l')
+end.
+
+Fixpoint app (P : forall {k k'}, alt_list k k' -> alt_list k k') {t1 t2} (l : alt_list t1 t2) {struct l}: forall {t3}, alt_list t2 t3 ->
+alt_list t1 t3 :=
+ match l with
+ | nil _ => fun _ l2 => P l2
+ | Ncons _ n l1 => fun _ l2 => Ncons n (app (@P) l1 l2)
+ | Bcons _ b l1 => fun _ l2 => Bcons b (app (@P) l1 l2)
+ end.
+
+Check (fun {t t'} (l: alt_list t t') =>
+ app trullynul (goodid l) (wrongid _ nil)).
diff --git a/test-suite/bugs/closed/shouldsucceed/2734.v b/test-suite/bugs/closed/shouldsucceed/2734.v
new file mode 100644
index 00000000..826361be
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2734.v
@@ -0,0 +1,15 @@
+Require Import Arith List.
+Require Import OrderedTypeEx.
+
+Module Adr.
+ Include Nat_as_OT.
+ Definition nat2t (i: nat) : t := i.
+End Adr.
+
+Inductive expr := Const: Adr.t -> expr.
+
+Inductive control := Go: expr -> control.
+
+Definition program := (Adr.t * (control))%type.
+
+Fail Definition myprog : program := (Adr.nat2t 0, Go (Adr.nat2t 0) ). \ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2750.v b/test-suite/bugs/closed/shouldsucceed/2750.v
new file mode 100644
index 00000000..fc580f10
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2750.v
@@ -0,0 +1,23 @@
+
+Module Type ModWithRecord.
+
+ Record foo : Type :=
+ { A : nat
+ ; B : nat
+ }.
+End ModWithRecord.
+
+Module Test_ModWithRecord (M : ModWithRecord).
+
+ Definition test1 : M.foo :=
+ {| M.A := 0
+ ; M.B := 2
+ |}.
+
+ Module B := M.
+
+ Definition test2 : M.foo :=
+ {| M.A := 0
+ ; M.B := 2
+ |}.
+End Test_ModWithRecord. \ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2817.v b/test-suite/bugs/closed/shouldsucceed/2817.v
new file mode 100644
index 00000000..08dff992
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2817.v
@@ -0,0 +1,9 @@
+(** Occur-check for Meta (up to application of already known instances) *)
+
+Goal forall (f: nat -> nat -> Prop) (x:bool)
+ (H: forall (u: nat), f u u -> True)
+ (H0: forall x0, f (if x then x0 else x0) x0),
+False.
+
+intros.
+Fail apply H in H0. (* should fail without exhausting the stack *)
diff --git a/test-suite/bugs/closed/shouldsucceed/2836.v b/test-suite/bugs/closed/shouldsucceed/2836.v
new file mode 100644
index 00000000..a948b75e
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2836.v
@@ -0,0 +1,39 @@
+(* Check that possible instantiation made during evar materialization
+ are taken into account and do not raise Not_found *)
+
+Set Implicit Arguments.
+
+Record SpecializedCategory (obj : Type) (Morphism : obj -> obj -> Type) := {
+ Object :> _ := obj;
+
+ Identity' : forall o, Morphism o o;
+ Compose' : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
+}.
+
+Section SpecializedCategoryInterface.
+ Variable obj : Type.
+ Variable mor : obj -> obj -> Type.
+ Variable C : @SpecializedCategory obj mor.
+
+ Definition Morphism (s d : C) := mor s d.
+ Definition Identity (o : C) : Morphism o o := C.(Identity') o.
+ Definition Compose (s d d' : C) (m : Morphism d d') (m0 : Morphism s d) :
+Morphism s d' := C.(Compose') s d d' m m0.
+End SpecializedCategoryInterface.
+
+Section ProductCategory.
+ Variable objC : Type.
+ Variable morC : objC -> objC -> Type.
+ Variable objD : Type.
+ Variable morD : objD -> objD -> Type.
+ Variable C : SpecializedCategory morC.
+ Variable D : SpecializedCategory morD.
+
+(* Should fail nicely *)
+Definition ProductCategory : @SpecializedCategory (objC * objD)%type (fun s d
+=> (morC (fst s) (fst d) * morD (snd s) (snd d))%type).
+Fail refine {|
+ Identity' := (fun o => (Identity (fst o), Identity (snd o)));
+ Compose' := (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd
+m2) (snd m1)))
+ |}.
diff --git a/test-suite/bugs/closed/shouldsucceed/2928.v b/test-suite/bugs/closed/shouldsucceed/2928.v
new file mode 100644
index 00000000..21e92ae2
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2928.v
@@ -0,0 +1,11 @@
+Class Equiv A := equiv: A -> A -> Prop.
+Infix "=" := equiv : type_scope.
+
+Class Associative {A} f `{Equiv A} := associativity x y z : f x (f y z) = f (f x y) z.
+
+Class SemiGroup A op `{Equiv A} := { sg_ass :>> Associative op }.
+
+Class SemiLattice A op `{Equiv A} :=
+ { semilattice_sg :>> SemiGroup A op
+ ; redundant : Associative op
+ }.
diff --git a/test-suite/bugs/closed/shouldsucceed/2983.v b/test-suite/bugs/closed/shouldsucceed/2983.v
new file mode 100644
index 00000000..15598352
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2983.v
@@ -0,0 +1,8 @@
+Module Type ModA.
+End ModA.
+Module Type ModB(A : ModA).
+End ModB.
+Module Foo(A : ModA)(B : ModB A).
+End Foo.
+
+Print Module Foo. \ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2995.v b/test-suite/bugs/closed/shouldsucceed/2995.v
new file mode 100644
index 00000000..ba3acd08
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2995.v
@@ -0,0 +1,9 @@
+Module Type Interface.
+ Parameter error: nat.
+End Interface.
+
+Module Implementation <: Interface.
+ Definition t := bool.
+ Definition error: t := false.
+Fail End Implementation.
+(* A UserError here is expected, not an uncaught Not_found *) \ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/3000.v b/test-suite/bugs/closed/shouldsucceed/3000.v
new file mode 100644
index 00000000..27de34ed
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/3000.v
@@ -0,0 +1,2 @@
+Inductive t (t':Type) : Type := A | B.
+Definition d := match t with _ => 1 end. (* used to fail on list_chop *)
diff --git a/test-suite/bugs/closed/shouldsucceed/3004.v b/test-suite/bugs/closed/shouldsucceed/3004.v
new file mode 100644
index 00000000..896b1958
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/3004.v
@@ -0,0 +1,7 @@
+Set Implicit Arguments.
+Unset Strict Implicit.
+Parameter (M : nat -> Type).
+Parameter (mp : forall (T1 T2 : Type) (f : T1 -> T2), list T1 -> list T2).
+
+Definition foo (s : list {n : nat & M n}) :=
+ let exT := existT in mp (fun x => projT1 x) s.
diff --git a/test-suite/bugs/closed/shouldsucceed/3008.v b/test-suite/bugs/closed/shouldsucceed/3008.v
new file mode 100644
index 00000000..3f3a979a
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/3008.v
@@ -0,0 +1,29 @@
+Module Type Intf1.
+Parameter T : Type.
+Inductive a := A.
+End Intf1.
+
+Module Impl1 <: Intf1.
+Definition T := unit.
+Inductive a := A.
+End Impl1.
+
+Module Type Intf2
+ (Impl1 : Intf1).
+Parameter x : Impl1.A=Impl1.A -> Impl1.T.
+End Intf2.
+
+Module Type Intf3
+ (Impl1 : Intf1)
+ (Impl2 : Intf2(Impl1)).
+End Intf3.
+
+Fail Module Toto
+ (Impl1' : Intf1)
+ (Impl2 : Intf2(Impl1'))
+ (Impl3 : Intf3(Impl1)(Impl2)).
+(* A UserError is expected here, not an uncaught Not_found *)
+
+(* NB : the Inductive above and the A=A weren't in the initial test,
+ they are here only to force an access to the environment
+ (cf [Printer.qualid_of_global]) and check that this env is ok. *) \ No newline at end of file