1 files changed, 0 insertions, 174 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1834.v b/test-suite/bugs/closed/shouldsucceed/1834.v
deleted file mode 100644
index 947d15f0..00000000
--- a/test-suite/bugs/closed/shouldsucceed/1834.v
+++ /dev/null
@@ -1,174 +0,0 @@
-(* 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.