Imported Upstream snapshot 8.3~beta0+13298

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. *)