summaryrefslogtreecommitdiff
path: root/test-suite/failure
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/failure')
-rw-r--r--test-suite/failure/Case5.v2
-rw-r--r--test-suite/failure/Case9.v2
-rw-r--r--test-suite/failure/ImportedCoercion.v7
-rw-r--r--test-suite/failure/Sections.v4
-rw-r--r--test-suite/failure/evar1.v3
-rw-r--r--test-suite/failure/evarlemma.v3
-rw-r--r--test-suite/failure/fixpoint3.v13
-rw-r--r--test-suite/failure/fixpoint4.v19
-rw-r--r--test-suite/failure/guard.v2
-rw-r--r--test-suite/failure/inductive3.v2
-rw-r--r--test-suite/failure/proofirrelevance.v2
-rw-r--r--test-suite/failure/rewrite_in_hyp2.v2
-rw-r--r--test-suite/failure/subtyping.v6
-rw-r--r--test-suite/failure/subtyping2.v8
-rw-r--r--test-suite/failure/univ_include.v4
-rw-r--r--test-suite/failure/universes-buraliforti-redef.v8
-rw-r--r--test-suite/failure/universes-buraliforti.v8
-rw-r--r--test-suite/failure/universes3.v25
18 files changed, 97 insertions, 23 deletions
diff --git a/test-suite/failure/Case5.v b/test-suite/failure/Case5.v
index 29996fd4..494443f1 100644
--- a/test-suite/failure/Case5.v
+++ b/test-suite/failure/Case5.v
@@ -1,7 +1,7 @@
Inductive MS : Set :=
| X : MS -> MS
| Y : MS -> MS.
-
+
Type (fun p : MS => match p return nat with
| X x => 0
end).
diff --git a/test-suite/failure/Case9.v b/test-suite/failure/Case9.v
index a3b99f63..d63c4940 100644
--- a/test-suite/failure/Case9.v
+++ b/test-suite/failure/Case9.v
@@ -1,7 +1,7 @@
Parameter compare : forall n m : nat, {n < m} + {n = m} + {n > m}.
Type
match compare 0 0 return nat with
-
+
(* k<i *) | left _ _ (left _ _ _) => 0
(* k=i *) | left _ _ _ => 0
(* k>i *) | right _ _ _ => 0
diff --git a/test-suite/failure/ImportedCoercion.v b/test-suite/failure/ImportedCoercion.v
new file mode 100644
index 00000000..0a69b851
--- /dev/null
+++ b/test-suite/failure/ImportedCoercion.v
@@ -0,0 +1,7 @@
+(* Test visibility of coercions *)
+
+Require Import make_local.
+
+(* Local coercion must not be used *)
+
+Check (0 = true).
diff --git a/test-suite/failure/Sections.v b/test-suite/failure/Sections.v
new file mode 100644
index 00000000..9b3b35c1
--- /dev/null
+++ b/test-suite/failure/Sections.v
@@ -0,0 +1,4 @@
+Module A.
+Section B.
+End A.
+End A.
diff --git a/test-suite/failure/evar1.v b/test-suite/failure/evar1.v
new file mode 100644
index 00000000..1a4e42a8
--- /dev/null
+++ b/test-suite/failure/evar1.v
@@ -0,0 +1,3 @@
+(* This used to succeed by producing an ill-typed term in v8.2 *)
+
+Lemma u: forall A : Prop, (exist _ A A) = (exist _ A A).
diff --git a/test-suite/failure/evarlemma.v b/test-suite/failure/evarlemma.v
new file mode 100644
index 00000000..ea753e79
--- /dev/null
+++ b/test-suite/failure/evarlemma.v
@@ -0,0 +1,3 @@
+(* Check success of inference of evars in the context of lemmas *)
+
+Lemma foo x : True.
diff --git a/test-suite/failure/fixpoint3.v b/test-suite/failure/fixpoint3.v
new file mode 100644
index 00000000..42f06916
--- /dev/null
+++ b/test-suite/failure/fixpoint3.v
@@ -0,0 +1,13 @@
+(* Check that arguments of impredicative types are not considered
+ subterms for the guard condition (an example by Thierry Coquand) *)
+
+Inductive I : Prop :=
+| C: (forall P:Prop, P->P) -> I.
+
+Definition i0 := C (fun _ x => x).
+
+Definition Paradox : False :=
+ (fix ni i : False :=
+ match i with
+ | C f => ni (f _ i)
+ end) i0.
diff --git a/test-suite/failure/fixpoint4.v b/test-suite/failure/fixpoint4.v
new file mode 100644
index 00000000..fd956373
--- /dev/null
+++ b/test-suite/failure/fixpoint4.v
@@ -0,0 +1,19 @@
+(* Check that arguments of impredicative types are not considered
+ subterms even through commutative cuts on functional arguments
+ (example prepared by Bruno) *)
+
+Inductive IMP : Prop :=
+ CIMP : (forall A:Prop, A->A) -> IMP
+| LIMP : (nat->IMP)->IMP.
+
+Definition i0 := (LIMP (fun _ => CIMP (fun _ x => x))).
+
+Definition Paradox : False :=
+ (fix F y o {struct o} : False :=
+ match y with
+ | tt => fun f =>
+ match f 0 with
+ | CIMP h => F y (h _ o)
+ | _ => F y (f 0)
+ end
+ end match o with LIMP f => f | _ => fun _ => o end) tt i0.
diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v
index 7e07a905..75e51138 100644
--- a/test-suite/failure/guard.v
+++ b/test-suite/failure/guard.v
@@ -18,4 +18,4 @@ Definition f :=
let h := f in (* h = Rel 4 *)
fix F (n:nat) : nat :=
h F S n. (* here Rel 4 = g *)
-
+
diff --git a/test-suite/failure/inductive3.v b/test-suite/failure/inductive3.v
index e5a4e1b6..cf035edf 100644
--- a/test-suite/failure/inductive3.v
+++ b/test-suite/failure/inductive3.v
@@ -1,4 +1,4 @@
-(* Check that the nested inductive types positivity check avoids recursively
+(* Check that the nested inductive types positivity check avoids recursively
non uniform parameters (at least if these parameters break positivity) *)
Inductive t (A:Type) : Type := c : t (A -> A) -> t A.
diff --git a/test-suite/failure/proofirrelevance.v b/test-suite/failure/proofirrelevance.v
index eedf2612..93e159e8 100644
--- a/test-suite/failure/proofirrelevance.v
+++ b/test-suite/failure/proofirrelevance.v
@@ -1,5 +1,5 @@
(* This was working in version 8.1beta (bug in the Sort-polymorphism
- of inductive types), but this is inconsistent with classical logic
+ of inductive types), but this is inconsistent with classical logic
in Prop *)
Inductive bool_in_prop : Type := hide : bool -> bool_in_prop
diff --git a/test-suite/failure/rewrite_in_hyp2.v b/test-suite/failure/rewrite_in_hyp2.v
index a32037a2..1533966e 100644
--- a/test-suite/failure/rewrite_in_hyp2.v
+++ b/test-suite/failure/rewrite_in_hyp2.v
@@ -1,4 +1,4 @@
-(* Until revision 10221, rewriting in hypotheses of the form
+(* Until revision 10221, rewriting in hypotheses of the form
"(fun x => phi(x)) t" with "t" not rewritable used to behave as a
beta-normalization tactic instead of raising the expected message
"nothing to rewrite" *)
diff --git a/test-suite/failure/subtyping.v b/test-suite/failure/subtyping.v
index 35fd2036..127da851 100644
--- a/test-suite/failure/subtyping.v
+++ b/test-suite/failure/subtyping.v
@@ -4,17 +4,17 @@ Module Type T.
Parameter A : Type.
- Inductive L : Prop :=
+ Inductive L : Prop :=
| L0
| L1 : (A -> Prop) -> L.
End T.
-Module TT : T.
+Module TT : T.
Parameter A : Type.
- Inductive L : Type :=
+ Inductive L : Type :=
| L0
| L1 : (A -> Prop) -> L.
diff --git a/test-suite/failure/subtyping2.v b/test-suite/failure/subtyping2.v
index 0a75ae45..addd3b45 100644
--- a/test-suite/failure/subtyping2.v
+++ b/test-suite/failure/subtyping2.v
@@ -61,7 +61,7 @@ End Inverse_Image.
Section Burali_Forti_Paradox.
- Definition morphism (A : Type) (R : A -> A -> Prop)
+ Definition morphism (A : Type) (R : A -> A -> Prop)
(B : Type) (S : B -> B -> Prop) (f : A -> B) :=
forall x y : A, R x y -> S (f x) (f y).
@@ -69,7 +69,7 @@ Section Burali_Forti_Paradox.
assumes there exists an universal system of notations, i.e:
- A type A0
- An injection i0 from relations on any type into A0
- - The proof that i0 is injective modulo morphism
+ - The proof that i0 is injective modulo morphism
*)
Variable A0 : Type. (* Type_i *)
Variable i0 : forall X : Type, (X -> X -> Prop) -> A0. (* X: Type_j *)
@@ -82,7 +82,7 @@ Section Burali_Forti_Paradox.
(* Embedding of x in y: x and y are images of 2 well founded relations
R1 and R2, the ordinal of R2 being strictly greater than that of R1.
*)
- Record emb (x y : A0) : Prop :=
+ Record emb (x y : A0) : Prop :=
{X1 : Type;
R1 : X1 -> X1 -> Prop;
eqx : x = i0 X1 R1;
@@ -166,7 +166,7 @@ Defined.
End Subsets.
- Definition fsub (a b : A0) (H : emb a b) (x : sub a) :
+ Definition fsub (a b : A0) (H : emb a b) (x : sub a) :
sub b := Build_sub _ (witness _ x) (emb_trans _ _ _ (emb_wit _ x) H).
(* F is a morphism: a < b => F(a) < F(b)
diff --git a/test-suite/failure/univ_include.v b/test-suite/failure/univ_include.v
index 4be70d88..56f04f9d 100644
--- a/test-suite/failure/univ_include.v
+++ b/test-suite/failure/univ_include.v
@@ -1,9 +1,9 @@
Definition T := Type.
Definition U := Type.
-Module Type MT.
+Module Type MT.
Parameter t : T.
-End MT.
+End MT.
Module Type MU.
Parameter t : U.
diff --git a/test-suite/failure/universes-buraliforti-redef.v b/test-suite/failure/universes-buraliforti-redef.v
index 049f97f2..034b7f09 100644
--- a/test-suite/failure/universes-buraliforti-redef.v
+++ b/test-suite/failure/universes-buraliforti-redef.v
@@ -64,7 +64,7 @@ End Inverse_Image.
Section Burali_Forti_Paradox.
- Definition morphism (A : Type) (R : A -> A -> Prop)
+ Definition morphism (A : Type) (R : A -> A -> Prop)
(B : Type) (S : B -> B -> Prop) (f : A -> B) :=
forall x y : A, R x y -> S (f x) (f y).
@@ -72,7 +72,7 @@ Section Burali_Forti_Paradox.
assumes there exists an universal system of notations, i.e:
- A type A0
- An injection i0 from relations on any type into A0
- - The proof that i0 is injective modulo morphism
+ - The proof that i0 is injective modulo morphism
*)
Variable A0 : Type. (* Type_i *)
Variable i0 : forall X : Type, (X -> X -> Prop) -> A0. (* X: Type_j *)
@@ -85,7 +85,7 @@ Section Burali_Forti_Paradox.
(* Embedding of x in y: x and y are images of 2 well founded relations
R1 and R2, the ordinal of R2 being strictly greater than that of R1.
*)
- Record emb (x y : A0) : Prop :=
+ Record emb (x y : A0) : Prop :=
{X1 : Type;
R1 : X1 -> X1 -> Prop;
eqx : x = i0 X1 R1;
@@ -168,7 +168,7 @@ Defined.
End Subsets.
- Definition fsub (a b : A0) (H : emb a b) (x : sub a) :
+ Definition fsub (a b : A0) (H : emb a b) (x : sub a) :
sub b := Build_sub _ (witness _ x) (emb_trans _ _ _ (emb_wit _ x) H).
(* F is a morphism: a < b => F(a) < F(b)
diff --git a/test-suite/failure/universes-buraliforti.v b/test-suite/failure/universes-buraliforti.v
index d18d2119..1f96ab34 100644
--- a/test-suite/failure/universes-buraliforti.v
+++ b/test-suite/failure/universes-buraliforti.v
@@ -47,7 +47,7 @@ End Inverse_Image.
Section Burali_Forti_Paradox.
- Definition morphism (A : Type) (R : A -> A -> Prop)
+ Definition morphism (A : Type) (R : A -> A -> Prop)
(B : Type) (S : B -> B -> Prop) (f : A -> B) :=
forall x y : A, R x y -> S (f x) (f y).
@@ -55,7 +55,7 @@ Section Burali_Forti_Paradox.
assumes there exists an universal system of notations, i.e:
- A type A0
- An injection i0 from relations on any type into A0
- - The proof that i0 is injective modulo morphism
+ - The proof that i0 is injective modulo morphism
*)
Variable A0 : Type. (* Type_i *)
Variable i0 : forall X : Type, (X -> X -> Prop) -> A0. (* X: Type_j *)
@@ -68,7 +68,7 @@ Section Burali_Forti_Paradox.
(* Embedding of x in y: x and y are images of 2 well founded relations
R1 and R2, the ordinal of R2 being strictly greater than that of R1.
*)
- Record emb (x y : A0) : Prop :=
+ Record emb (x y : A0) : Prop :=
{X1 : Type;
R1 : X1 -> X1 -> Prop;
eqx : x = i0 X1 R1;
@@ -152,7 +152,7 @@ Defined.
End Subsets.
- Definition fsub (a b : A0) (H : emb a b) (x : sub a) :
+ Definition fsub (a b : A0) (H : emb a b) (x : sub a) :
sub b := Build_sub _ (witness _ x) (emb_trans _ _ _ (emb_wit _ x) H).
(* F is a morphism: a < b => F(a) < F(b)
diff --git a/test-suite/failure/universes3.v b/test-suite/failure/universes3.v
new file mode 100644
index 00000000..8fb414d5
--- /dev/null
+++ b/test-suite/failure/universes3.v
@@ -0,0 +1,25 @@
+(* This example (found by coqchk) checks that an inductive cannot be
+ polymorphic if its constructors induce upper universe constraints.
+ Here: I cannot be polymorphic because its type is less than the
+ type of the argument of impl. *)
+
+Definition Type1 := Type.
+Definition Type3 : Type1 := Type. (* Type3 < Type1 *)
+Definition Type4 := Type.
+Definition impl (A B:Type3) : Type4 := A->B. (* Type3 <= Type4 *)
+Inductive I (B:Type (*6*)) := C : B -> impl Prop (I B).
+ (* Type(6) <= Type(7) because I contains, via C, elements in B
+ Type(7) <= Type3 because (I B) is argument of impl
+ Type(4) <= Type(7) because type of C less than I (see remark below)
+
+ where Type(7) is the auxiliary level used to infer the type of I
+*)
+
+(* We cannot enforce Type1 < Type(6) while we already have
+ Type(6) <= Type(7) < Type3 < Type1 *)
+Definition J := I Type1.
+
+(* Open question: should the type of an inductive be the max of the
+ types of the _arguments_ of its constructors (here B and Prop,
+ after unfolding of impl), or of the max of types of the
+ constructors itself (here B -> impl Prop (I B)), as done above. *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 03:17:21 +0000