Merge branch 'v8.5' into trunk

4 files changed, 24 insertions, 14 deletions

diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index b29f06c65..49ab68bea 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -57,11 +57,14 @@ let set_global v =
 
 let rec eq_structured_constant c1 c2 = match c1, c2 with
 | Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2
+| Const_sorts _, _ -> false
 | Const_ind i1, Const_ind i2 -> Univ.eq_puniverses eq_ind i1 i2
+| Const_ind _, _ -> false
 | Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2
+| Const_b0 _, _ -> false
 | Const_bn (t1, a1), Const_bn (t2, a2) ->
   Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2
-| _ -> false
+| Const_bn _, _ -> false
 
 let rec hash_structured_constant c =
   let open Hashset.Combine in
diff --git a/kernel/names.ml b/kernel/names.ml
index 480b37e89..f217c932c 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -819,6 +819,10 @@ struct
   let map f (c, b as x) =
     let c' = f c in
       if c' == c then x else (c', b)
+
+  let to_string p = Constant.to_string (constant p)
+  let print p = Constant.print (constant p)
+
 end
 
 type projection = Projection.t
diff --git a/kernel/names.mli b/kernel/names.mli
index 92ee58f26..7cc444375 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -652,6 +652,10 @@ module Projection : sig
   val compare : t -> t -> int
     
   val map : (constant -> constant) -> t -> t
+
+  val to_string : t -> string
+  val print : t -> Pp.std_ppcmds
+
 end
 
 type projection = Projection.t
diff --git a/kernel/univ.ml b/kernel/univ.ml
index fce9e28d3..1d82be63b 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -925,7 +925,8 @@ let fast_compare_neq strict g arcu arcv =
     if arc_is_lt arc then
       cmp c to_revert lt_todo le_todo
     else
-      process_lt c to_revert lt_todo le_todo arc arc.lt arc.le
+      let () = arc.status <- SetLt in
+      process_lt c (arc :: to_revert) lt_todo le_todo arc.lt arc.le
   | [], arc::le_todo ->
     if arc == arcv then
       (* No need to continue inspecting universes above arc:
@@ -937,40 +938,38 @@ let fast_compare_neq strict g arcu arcv =
       if arc_is_le arc then
         cmp c to_revert [] le_todo
       else
-        process_le c to_revert [] le_todo arc arc.lt
+        let () = arc.status <- SetLe in
+        process_le c (arc :: to_revert) [] le_todo arc.lt arc.le
 
-  and process_lt c to_revert lt_todo le_todo arc0 lt le = match le with
+  and process_lt c to_revert lt_todo le_todo lt le = match le with
   | [] ->
     begin match lt with
-    | [] ->
-      let () = arc0.status <- SetLt in
-      cmp c (arc0 :: to_revert) lt_todo le_todo
+    | [] -> cmp c to_revert lt_todo le_todo
     | u :: lt ->
       let arc = repr g u in
       if arc == arcv then
         if strict then (to_revert, FastLT) else (to_revert, FastLE)
-      else process_lt c to_revert (arc :: lt_todo) le_todo arc0 lt le
+      else process_lt c to_revert (arc :: lt_todo) le_todo lt le
     end
   | u :: le ->
     let arc = repr g u in
     if arc == arcv then
       if strict then (to_revert, FastLT) else (to_revert, FastLE)
-    else process_lt c to_revert (arc :: lt_todo) le_todo arc0 lt le
+    else process_lt c to_revert (arc :: lt_todo) le_todo lt le
 
-  and process_le c to_revert lt_todo le_todo arc0 lt = match lt with
+  and process_le c to_revert lt_todo le_todo lt le = match lt with
   | [] ->
     let fold accu u =
       let node = repr g u in
       node :: accu
     in
-    let le_new = List.fold_left fold le_todo arc0.le in
-    let () = arc0.status <- SetLe in
-    cmp c (arc0 :: to_revert) lt_todo le_new
+    let le_new = List.fold_left fold le_todo le in
+    cmp c to_revert lt_todo le_new
   | u :: lt ->
     let arc = repr g u in
     if arc == arcv then
       if strict then (to_revert, FastLT) else (to_revert, FastLE)
-    else process_le c to_revert (arc :: lt_todo) le_todo arc0 lt
+    else process_le c to_revert (arc :: lt_todo) le_todo lt le
 
   in