From dd96b1e5e8d0eb9f93cff423b6f9cf900aee49d7 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 30 May 2014 20:55:48 +0200
Subject: - Fix hashing of levels to get the "right" order in universe contexts
 etc... - Add a tentative syntax for specifying universes: Type{"i"} and
 foo@{Type{"i"},Type{"j"}}. These are always rigid. - Use level-to-level
 substitutions where the more general level-to-universe substitutions were
 previously used.

---
 test-suite/success/polymorphism.v | 27 ++++++++++++++++++++++++++-
 1 file changed, 26 insertions(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 99284eb547..fd299b43ad 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -1,3 +1,28 @@
+Module withoutpoly.
+
+Inductive empty :=. 
+
+Inductive emptyt : Type :=. 
+Inductive singleton : Type :=
+  single.
+Inductive singletoninfo : Type :=
+  singleinfo : unit -> singletoninfo.
+Inductive singletonset : Set :=
+  singleset.
+
+Inductive singletonnoninfo : Type :=
+  singlenoninfo : empty -> singletonnoninfo.
+
+Inductive singletoninfononinfo : Prop :=
+  singleinfononinfo : unit -> singletoninfononinfo.
+
+Inductive bool : Type := 
+  | true | false.
+
+Inductive smashedbool : Prop := 
+  | trueP | falseP.
+End withoutpoly.
+
 Set Universe Polymorphism.
 
 Inductive empty :=. 
@@ -225,7 +250,7 @@ Fail Check fun A : Type => foo A.
 Check fun A : Prop => foo A.
 Fail Definition bar := fun A : Set => foo A.
 
-Fail Check (let A := Type in foo (id A)).
+Check (let A := Type in foo (id A)).
 
 Definition fooS (A : Set) := A.
 
-- 
cgit v1.2.3