Merge branch 'v8.5'

2 files changed, 43 insertions, 39 deletions

diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index ae86d686ae..e2854abfd3 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -26,8 +26,8 @@ let univ_of_sort = function
   | Prop Null -> Universe.type0m
 
 let sort_of_univ u =
-  if is_type0m_univ u then Prop Null
-  else if is_type0_univ u then Prop Pos
+  if is_type0m_univ u then prop
+  else if is_type0_univ u then set
   else Type u
 
 let compare s1 s2 =
@@ -62,6 +62,8 @@ let is_small = function
 let family = function
   | Prop Null -> InProp
   | Prop Pos -> InSet
+  | Type u when is_type0m_univ u -> InProp
+  | Type u when is_type0_univ u -> InSet
   | Type _ -> InType
 
 let family_equal = (==)
@@ -76,7 +78,7 @@ let hash = function
   in
   combinesmall 1 h
 | Type u ->
-  let h = Hashtbl.hash u in (** FIXME *)
+ let h = Univ.Universe.hash u in
   combinesmall 2 h
 
 module List = struct
@@ -101,7 +103,7 @@ module Hsorts =
         | (Type u1, Type u2) -> u1 == u2
         |_ -> false
 
-      let hash = Hashtbl.hash (** FIXME *)
+      let hash = hash
     end)
 
 let hcons = Hashcons.simple_hcons Hsorts.generate Hsorts.hcons hcons_univ
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 4af7fe7c1c..fce9e28d36 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -925,25 +925,7 @@ let fast_compare_neq strict g arcu arcv =
     if arc_is_lt arc then
       cmp c to_revert lt_todo le_todo
     else
-      let rec find lt_todo lt le = match le with
-      | [] ->
-        begin match lt with
-        | [] ->
-          let () = arc.status <- SetLt in
-          cmp c (arc :: 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 find (arc :: lt_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 find (arc :: lt_todo) lt le
-      in
-      find lt_todo arc.lt arc.le
+      process_lt c to_revert lt_todo le_todo arc arc.lt arc.le
   | [], arc::le_todo ->
     if arc == arcv then
       (* No need to continue inspecting universes above arc:
@@ -955,23 +937,43 @@ let fast_compare_neq strict g arcu arcv =
       if arc_is_le arc then
         cmp c to_revert [] le_todo
       else
-        let rec find lt_todo lt = 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 arc.le in
-          let () = arc.status <- SetLe in
-          cmp c (arc :: 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 find (arc :: lt_todo) lt
-        in
-        find [] arc.lt
+        process_le c to_revert [] le_todo arc arc.lt
+
+  and process_lt c to_revert lt_todo le_todo arc0 lt le = match le with
+  | [] ->
+    begin match lt with
+    | [] ->
+      let () = arc0.status <- SetLt in
+      cmp c (arc0 :: 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
+    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
+
+  and process_le c to_revert lt_todo le_todo arc0 lt = 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
+  | 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
+
   in
+
   try
     let (to_revert, c) = cmp FastNLE [] [] [arcu] in
     (** Reset all the touched arcs. *)