Merge branch 'v8.6'

6 files changed, 64 insertions, 40 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 47df22807..5dec3b785 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -23,9 +23,9 @@
 #include "coq_values.h" 
 
 /* spiwack: I append here a few macros for value/number manipulation */
-#define uint32_of_value(val) ((uint32_t)(val) >> 1)
-#define value_of_uint32(i)   ((value)(((uint32_t)(i) << 1) | 1))
-#define UI64_of_uint32(lo) ((uint64_t)(lo))
+#define uint32_of_value(val) (((uint32_t)(val)) >> 1)
+#define value_of_uint32(i)   ((value)((((uint32_t)(i)) << 1) | 1))
+#define UI64_of_uint32(lo) ((uint64_t)((uint32_t)(lo)))
 #define UI64_of_value(val) (UI64_of_uint32(uint32_of_value(val)))
 /* /spiwack */
 
diff --git a/kernel/names.ml b/kernel/names.ml
index d928d300f..1f138581c 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -34,9 +34,15 @@ struct
 
   let hash = String.hash
 
+  let warn_invalid_identifier =
+    CWarnings.create ~name:"invalid-identifier" ~category:"parsing"
+                     ~default:CWarnings.Disabled
+                     (fun s -> str s)
+
   let check_soft ?(warn = true) x =
     let iter (fatal, x) =
-      if fatal then CErrors.error x else if warn then Feedback.msg_warning (str x)
+      if fatal then CErrors.error x else
+        if warn then warn_invalid_identifier x
     in
     Option.iter iter (Unicode.ident_refutation x)
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 6c664f791..1ae89347a 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -316,7 +316,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
       (try
 	 let cuniv = conv_table_key infos fl1 fl2 cuniv in
 	   convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
-       with NotConvertible ->
+       with NotConvertible | Univ.UniverseInconsistency _ ->
            (* else the oracle tells which constant is to be expanded *)
 	 let oracle = CClosure.oracle_of_infos infos in
          let (app1,app2) =
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 9812c45f7..8a2b2469d 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -36,7 +36,7 @@ type 'a extended_conversion_function =
 type conv_pb = CONV | CUMUL
 
 type 'a universe_compare = 
-  { (* Might raise NotConvertible *)
+  { (* Might raise NotConvertible or UnivInconsistency *)
     compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a;
     compare_instances: flex:bool -> 
 		       Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
@@ -56,9 +56,12 @@ constructors. *)
 val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t ->
   'a * 'a universe_compare -> 'a * 'a universe_compare
 
+(** These two never raise UnivInconsistency, inferred_universes
+    just gathers the constraints. *)
 val checked_universes : UGraph.t universe_compare
 val inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare
 
+(** These two functions can only raise NotConvertible *)
 val conv : constr extended_conversion_function
 
 val conv_leq : types extended_conversion_function
@@ -70,6 +73,9 @@ val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) ->
 val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> 
   ?ts:Names.transparent_state -> types infer_conversion_function
 
+(** Depending on the universe state functions, this might raise
+  [UniverseInconsistency] in addition to [NotConvertible] (for better error
+  messages). *)
 val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) ->
   Names.transparent_state -> (constr,'a) generic_conversion_function
 
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index e2712615b..4884d0deb 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -638,19 +638,6 @@ let check_smaller g strict u v =
 
 type 'a check_function = universes -> 'a -> 'a -> bool
 
-let check_equal_expr g x y =
-  x == y || (let (u, n) = x and (v, m) = y in 
-               Int.equal n m && check_equal g u v)
-
-let check_eq_univs g l1 l2 =
-  let f x1 x2 = check_equal_expr g x1 x2 in
-  let exists x1 l = Universe.exists (fun x2 -> f x1 x2) l in
-    Universe.for_all (fun x1 -> exists x1 l2) l1
-    && Universe.for_all (fun x2 -> exists x2 l1) l2
-
-let check_eq g u v =
-  Universe.equal u v || check_eq_univs g u v
-
 let check_smaller_expr g (u,n) (v,m) =
   let diff = n - m in
     match diff with
@@ -669,7 +656,13 @@ let real_check_leq g u v =
 let check_leq g u v =
   Universe.equal u v ||
     is_type0m_univ u ||
-    check_eq_univs g u v || real_check_leq g u v
+    real_check_leq g u v
+
+let check_eq_univs g l1 l2 =
+  real_check_leq g l1 l2 && real_check_leq g l2 l1
+
+let check_eq g u v =
+  Universe.equal u v || check_eq_univs g u v
 
 (* enforce_univ_eq g u v will force u=v if possible, will fail otherwise *)
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 9224ec48d..09f884ecd 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -468,15 +468,32 @@ struct
       else if Level.is_prop u then
 	hcons (Level.set,n+k)
       else hcons (u,n+k)
-	
+
+    type super_result =
+	SuperSame of bool
+        (* The level expressions are in cumulativity relation. boolean
+           indicates if left is smaller than right?  *)
+      | SuperDiff of int
+        (* The level expressions are unrelated, the comparison result
+           is canonical *)
+
+    (** [super u v] compares two level expressions,
+       returning [SuperSame] if they refer to the same level at potentially different
+       increments or [SuperDiff] if they are different. The booleans indicate if the
+       left expression is "smaller" than the right one in both cases. *)
     let super (u,n as x) (v,n' as y) =
       let cmp = Level.compare u v in
-	if Int.equal cmp 0 then 
-	  if n < n' then Inl true
-	  else Inl false
-	else if is_prop x then Inl true
-	else if is_prop y then Inl false
-	else Inr cmp
+	if Int.equal cmp 0 then SuperSame (n < n')
+	else
+	  match x, y with
+	  | (l,0), (l',0) ->
+	     let open RawLevel in
+	     (match Level.data l, Level.data l' with
+	      | Prop, Prop -> SuperSame false
+	      | Prop, _ -> SuperSame true
+	      | _, Prop -> SuperSame false
+	      | _, _ -> SuperDiff cmp)
+	  | _, _ -> SuperDiff cmp
 
     let to_string (v, n) =
       if Int.equal n 0 then Level.to_string v
@@ -598,24 +615,26 @@ struct
     | Nil, _ -> l2
     | _, Nil -> l1
     | Cons (h1, _, t1), Cons (h2, _, t2) ->
-      (match Expr.super h1 h2 with
-      | Inl true (* h1 < h2 *) -> merge_univs t1 l2
-      | Inl false -> merge_univs l1 t2
-      | Inr c -> 
-        if c <= 0 (* h1 < h2 is name order *)
-	then cons h1 (merge_univs t1 l2)
-	else cons h2 (merge_univs l1 t2))
+       let open Expr in
+       (match super h1 h2 with
+	| SuperSame true (* h1 < h2 *) -> merge_univs t1 l2
+	| SuperSame false -> merge_univs l1 t2
+	| SuperDiff c ->
+           if c <= 0 (* h1 < h2 is name order *)
+	   then cons h1 (merge_univs t1 l2)
+	   else cons h2 (merge_univs l1 t2))
 
   let sort u =
     let rec aux a l = 
       match l with
       | Cons (b, _, l') ->
-        (match Expr.super a b with
-	| Inl false -> aux a l'
-	| Inl true -> l
-	| Inr c ->
-	  if c <= 0 then cons a l
-	  else cons b (aux a l'))
+	let open Expr in
+        (match super a b with
+	 | SuperSame false -> aux a l'
+	 | SuperSame true -> l
+	 | SuperDiff c ->
+	    if c <= 0 then cons a l
+	    else cons b (aux a l'))
       | Nil -> cons a l
     in 
       fold (fun a acc -> aux a acc) u nil