Univs: entirely disallow instantiation of polymorphic constants with

Prop levels.

As they are typed assuming all variables are >= Set now, and this was
breaking an invariant in typing. Only one instance in the standard
library was used in Hurkens, which can be avoided easily. This also
avoids displaying unnecessary >= Set constraints everywhere.

1 files changed, 4 insertions, 2 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index dc0a4b43c..2b3a2bdb1 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1707,7 +1707,9 @@ struct
     else if Array.length y = 0 then x 
     else Array.append x y
 
-  let of_array a = a
+  let of_array a =
+    assert(Array.for_all (fun x -> not (Level.is_prop x)) a);
+    a
 
   let to_array a = a
 
@@ -1715,7 +1717,7 @@ struct
 
   let subst_fn fn t = 
     let t' = CArray.smartmap fn t in
-      if t' == t then t else t'
+      if t' == t then t else of_array t'
 
   let levels x = LSet.of_array x