summaryrefslogtreecommitdiff
path: root/test-suite/failure
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/failure')
-rw-r--r--test-suite/failure/Tauto.v2
-rw-r--r--test-suite/failure/Uminus.v4
-rw-r--r--test-suite/failure/clash_cons.v2
-rw-r--r--test-suite/failure/fixpoint1.v2
-rw-r--r--test-suite/failure/guard.v2
-rw-r--r--test-suite/failure/illtype1.v2
-rw-r--r--test-suite/failure/inductive4.v15
-rw-r--r--test-suite/failure/pattern.v2
-rw-r--r--test-suite/failure/positivity.v2
-rw-r--r--test-suite/failure/redef.v2
-rw-r--r--test-suite/failure/search.v2
-rw-r--r--test-suite/failure/subtyping2.v20
-rw-r--r--test-suite/failure/universes-buraliforti-redef.v20
-rw-r--r--test-suite/failure/universes-buraliforti.v20
-rw-r--r--test-suite/failure/universes2.v4
15 files changed, 56 insertions, 45 deletions
diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v
index 96e66a0d..cbe7473c 100644
--- a/test-suite/failure/Tauto.v
+++ b/test-suite/failure/Tauto.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/failure/Uminus.v b/test-suite/failure/Uminus.v
index 6866f19a..3c3bf375 100644
--- a/test-suite/failure/Uminus.v
+++ b/test-suite/failure/Uminus.v
@@ -31,7 +31,7 @@ Lemma Omega : forall i:U -> prop, induct i -> up (i WF).
Proof.
intros i y.
apply y.
-unfold le, WF, induct in |- *.
+unfold le, WF, induct.
intros x H0.
apply y.
exact H0.
@@ -39,7 +39,7 @@ Qed.
Lemma lemma1 : induct (fun u => down (I u)).
Proof.
-unfold induct in |- *.
+unfold induct.
intros x p.
intro q.
apply (q (fun u => down (I u)) p).
diff --git a/test-suite/failure/clash_cons.v b/test-suite/failure/clash_cons.v
index 3f8d8784..25d3c165 100644
--- a/test-suite/failure/clash_cons.v
+++ b/test-suite/failure/clash_cons.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/failure/fixpoint1.v b/test-suite/failure/fixpoint1.v
index e4ef6c95..6abf6332 100644
--- a/test-suite/failure/fixpoint1.v
+++ b/test-suite/failure/fixpoint1.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v
index e5915ab1..324dc603 100644
--- a/test-suite/failure/guard.v
+++ b/test-suite/failure/guard.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/failure/illtype1.v b/test-suite/failure/illtype1.v
index ed48c6c2..6c14c2c3 100644
--- a/test-suite/failure/illtype1.v
+++ b/test-suite/failure/illtype1.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/failure/inductive4.v b/test-suite/failure/inductive4.v
new file mode 100644
index 00000000..6ba36fd2
--- /dev/null
+++ b/test-suite/failure/inductive4.v
@@ -0,0 +1,15 @@
+(* This used to succeed in versions 8.1 to 8.3 *)
+
+Require Import Logic.
+Require Hurkens.
+Definition Ti := Type.
+Inductive prod (X Y:Ti) := pair : X -> Y -> prod X Y.
+Definition B : Prop := let F := prod True in F Prop. (* Aie! *)
+Definition p2b (P:Prop) : B := pair True Prop I P.
+Definition b2p (b:B) : Prop := match b with pair _ P => P end.
+Lemma L1 : forall A : Prop, b2p (p2b A) -> A.
+Proof (fun A x => x).
+Lemma L2 : forall A : Prop, A -> b2p (p2b A).
+Proof (fun A x => x).
+Check Hurkens.paradox B p2b b2p L1 L2.
+
diff --git a/test-suite/failure/pattern.v b/test-suite/failure/pattern.v
index 129c380e..a24beaa2 100644
--- a/test-suite/failure/pattern.v
+++ b/test-suite/failure/pattern.v
@@ -6,4 +6,4 @@ Variable P : forall m : nat, m = n -> Prop.
Goal forall p : n = n, P n p.
intro.
-pattern n, p in |- *.
+pattern n, p.
diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v
index c02661e0..03cc1109 100644
--- a/test-suite/failure/positivity.v
+++ b/test-suite/failure/positivity.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/failure/redef.v b/test-suite/failure/redef.v
index 71d49b58..0c39b276 100644
--- a/test-suite/failure/redef.v
+++ b/test-suite/failure/redef.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/failure/search.v b/test-suite/failure/search.v
index ebbd5ca0..38a62766 100644
--- a/test-suite/failure/search.v
+++ b/test-suite/failure/search.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/failure/subtyping2.v b/test-suite/failure/subtyping2.v
index addd3b45..48fc2fff 100644
--- a/test-suite/failure/subtyping2.v
+++ b/test-suite/failure/subtyping2.v
@@ -54,7 +54,7 @@ Section Inverse_Image.
Qed.
Lemma WF_inverse_image : WF B R -> WF A Rof.
- red in |- *; intros; apply ACC_inverse_image; auto.
+ red; intros; apply ACC_inverse_image; auto.
Qed.
End Inverse_Image.
@@ -104,7 +104,7 @@ generalize eqx0; clear eqx0.
elim eqy using eq_ind_r; intro.
case (inj _ _ _ _ eqx0); intros.
exists X1 R1 X3 R3 (fun x : X1 => f0 (x0 (f x))) maj0; trivial.
-red in |- *; auto.
+red; auto.
Defined.
@@ -122,7 +122,7 @@ apply sym_eq; assumption.
intros.
apply H1 with (y := f (x1 maj)) (f := fun x : X1 => f (x1 (f0 x)));
- try red in |- *; auto.
+ try red; auto.
Defined.
(* The embedding relation is well founded *)
@@ -158,7 +158,7 @@ Section Subsets.
exists sub (Rof _ _ emb witness) A0 emb witness a; trivial.
exact WF_emb.
-red in |- *; trivial.
+red; trivial.
exact emb_wit.
Defined.
@@ -174,7 +174,7 @@ End Subsets.
- the upper bound is a, which is in F(b) since a < b
*)
Lemma F_morphism : morphism A0 emb A0 emb F.
-red in |- *; intros.
+red; intros.
exists
(sub x)
(Rof _ _ emb (witness x))
@@ -185,10 +185,10 @@ exists
apply WF_inverse_image.
exact WF_emb.
-unfold morphism, Rof, fsub in |- *; simpl in |- *; intros.
+unfold morphism, Rof, fsub; simpl; intros.
trivial.
-unfold Rof, fsub in |- *; simpl in |- *; intros.
+unfold Rof, fsub; simpl; intros.
apply emb_wit.
Defined.
@@ -230,10 +230,10 @@ intros.
change
match i0' X1 R1, i0' X2 R2 with
| i0 x1 r1, i0 x2 r2 => exists f : _, morphism x1 r1 x2 r2 f
- end in |- *.
-case H; simpl in |- *.
+ end.
+case H; simpl.
exists (fun x : X1 => x).
-red in |- *; trivial.
+red; trivial.
Defined.
(* The following command raises 'Error: Universe Inconsistency'.
diff --git a/test-suite/failure/universes-buraliforti-redef.v b/test-suite/failure/universes-buraliforti-redef.v
index 034b7f09..a8b5b975 100644
--- a/test-suite/failure/universes-buraliforti-redef.v
+++ b/test-suite/failure/universes-buraliforti-redef.v
@@ -54,7 +54,7 @@ Section Inverse_Image.
Qed.
Lemma WF_inverse_image : WF B R -> WF A Rof.
- red in |- *; intros; apply ACC_inverse_image; auto.
+ red; intros; apply ACC_inverse_image; auto.
Qed.
End Inverse_Image.
@@ -106,7 +106,7 @@ generalize eqx0; clear eqx0.
elim eqy using eq_ind_r; intro.
case (inj _ _ _ _ eqx0); intros.
exists X1 R1 X4 R4 (fun x : X1 => f0 (x0 (f x))) maj0; trivial.
-red in |- *; auto.
+red; auto.
Defined.
@@ -124,7 +124,7 @@ apply sym_eq; assumption.
intros.
apply H1 with (y := f (x1 maj)) (f := fun x : X1 => f (x1 (f0 x)));
- try red in |- *; auto.
+ try red; auto.
Defined.
(* The embedding relation is well founded *)
@@ -160,7 +160,7 @@ Section Subsets.
exists sub (Rof _ _ emb witness) A0 emb witness a; trivial.
exact WF_emb.
-red in |- *; trivial.
+red; trivial.
exact emb_wit.
Defined.
@@ -176,7 +176,7 @@ End Subsets.
- the upper bound is a, which is in F(b) since a < b
*)
Lemma F_morphism : morphism A0 emb A0 emb F.
-red in |- *; intros.
+red; intros.
exists
(sub x)
(Rof _ _ emb (witness x))
@@ -187,10 +187,10 @@ exists
apply WF_inverse_image.
exact WF_emb.
-unfold morphism, Rof, fsub in |- *; simpl in |- *; intros.
+unfold morphism, Rof, fsub; simpl; intros.
trivial.
-unfold Rof, fsub in |- *; simpl in |- *; intros.
+unfold Rof, fsub; simpl; intros.
apply emb_wit.
Defined.
@@ -231,10 +231,10 @@ intros.
change
match i0 X1 R1, i0 X2 R2 with
| i1 x1 r1, i1 x2 r2 => exists f : _, morphism x1 r1 x2 r2 f
- end in |- *.
-case H; simpl in |- *.
+ end.
+case H; simpl.
exists (fun x : X1 => x).
-red in |- *; trivial.
+red; trivial.
Defined.
(* The following command raises 'Error: Universe Inconsistency'.
diff --git a/test-suite/failure/universes-buraliforti.v b/test-suite/failure/universes-buraliforti.v
index 1f96ab34..7b62a0c5 100644
--- a/test-suite/failure/universes-buraliforti.v
+++ b/test-suite/failure/universes-buraliforti.v
@@ -37,7 +37,7 @@ Section Inverse_Image.
Qed.
Lemma WF_inverse_image : WF B R -> WF A Rof.
- red in |- *; intros; apply ACC_inverse_image; auto.
+ red; intros; apply ACC_inverse_image; auto.
Qed.
End Inverse_Image.
@@ -90,7 +90,7 @@ generalize eqx0; clear eqx0.
elim eqy using eq_ind_r; intro.
case (inj _ _ _ _ eqx0); intros.
exists X1 R1 X3 R3 (fun x : X1 => f0 (x0 (f x))) maj0; trivial.
-red in |- *; auto.
+red; auto.
Defined.
@@ -108,7 +108,7 @@ apply sym_eq; assumption.
intros.
apply H1 with (y := f (x1 maj)) (f := fun x : X1 => f (x1 (f0 x)));
- try red in |- *; auto.
+ try red; auto.
Defined.
(* The embedding relation is well founded *)
@@ -144,7 +144,7 @@ Section Subsets.
exists sub (Rof _ _ emb witness) A0 emb witness a; trivial.
exact WF_emb.
-red in |- *; trivial.
+red; trivial.
exact emb_wit.
Defined.
@@ -160,7 +160,7 @@ End Subsets.
- the upper bound is a, which is in F(b) since a < b
*)
Lemma F_morphism : morphism A0 emb A0 emb F.
-red in |- *; intros.
+red; intros.
exists
(sub x)
(Rof _ _ emb (witness x))
@@ -171,10 +171,10 @@ exists
apply WF_inverse_image.
exact WF_emb.
-unfold morphism, Rof, fsub in |- *; simpl in |- *; intros.
+unfold morphism, Rof, fsub; simpl; intros.
trivial.
-unfold Rof, fsub in |- *; simpl in |- *; intros.
+unfold Rof, fsub; simpl; intros.
apply emb_wit.
Defined.
@@ -222,10 +222,10 @@ intros.
change
match i0 X1 R1, i0 X2 R2 with
| i0 x1 r1, i0 x2 r2 => exists f : _, morphism x1 r1 x2 r2 f
- end in |- *.
-case H; simpl in |- *.
+ end.
+case H; simpl.
exists (fun x : X1 => x).
-red in |- *; trivial.
+red; trivial.
Defined.
(* The following command raises 'Error: Universe Inconsistency'.
diff --git a/test-suite/failure/universes2.v b/test-suite/failure/universes2.v
deleted file mode 100644
index e74de70f..00000000
--- a/test-suite/failure/universes2.v
+++ /dev/null
@@ -1,4 +0,0 @@
-(* Example submitted by Randy Pollack *)
-
-Parameter K : forall T : Type, T -> T.
-Check (K (forall T : Type, T -> T) K).
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 14:45:58 +0000