Remove universe specific terminology from acyclicgraph

This means removing [univ], [level] and derived abbreviations like
[lvl].

We keep using u, v for variable names as doing otherwise would be too
intrusive, and it's not overly universe specific.

2 files changed, 199 insertions, 204 deletions

diff --git a/lib/acyclicGraph.ml b/lib/acyclicGraph.ml
index 9afee6f0fd..7d04c8f5a1 100644
--- a/lib/acyclicGraph.ml
+++ b/lib/acyclicGraph.ml
@@ -27,7 +27,7 @@ module type Point = sig
   val pr : t -> Pp.t
 end
 
-module Make (Level:Point) = struct
+module Make (Point:Point) = struct
 
   (* Created in Caml by Gérard Huet for CoC 4.8 [Dec 1988] *)
   (* Functional code by Jean-Christophe Filliâtre for Coq V7.0 [1999] *)
@@ -43,7 +43,7 @@ module Make (Level:Point) = struct
      $<$ between equivalence classes, and we maintain that $<$ is acyclic,
      and contained in $\le$ in the sense that $[U]<[V]$ implies $U\le V$.
 
-     At every moment, we have a finite number of universes, and we
+     At every moment, we have a finite number of points, and we
      maintain the ordering in the presence of assertions $U<V$ and $U\le V$.
 
      The equivalence $\~{}$ is represented by a tree structure, as in the
@@ -58,18 +58,18 @@ module Make (Level:Point) = struct
 
   *)
 
-  module LMap = Level.Map
-  module LSet = Level.Set
-  module Constraint = Level.Constraint
+  module PMap = Point.Map
+  module PSet = Point.Set
+  module Constraint = Point.Constraint
 
   type status = NoMark | Visited | WeakVisited | ToMerge
 
   (* Comparison on this type is pointer equality *)
   type canonical_node =
-    { univ: Level.t;
-      ltle: bool LMap.t;  (* true: strict (lt) constraint.
+    { canon: Point.t;
+      ltle: bool PMap.t;  (* true: strict (lt) constraint.
                              false: weak  (le) constraint. *)
-      gtge: LSet.t;
+      gtge: PSet.t;
       rank : int;
       klvl: int;
       ilvl: int;
@@ -78,44 +78,44 @@ module Make (Level:Point) = struct
 
   let big_rank = 1000000
 
-  (* A Level.t is either an alias for another one, or a canonical one,
-     for which we know the universes that are above *)
+  (* A Point.t is either an alias for another one, or a canonical one,
+     for which we know the points that are above *)
 
-  type univ_entry =
-      Canonical of canonical_node
-    | Equiv of Level.t
+  type entry =
+    | Canonical of canonical_node
+    | Equiv of Point.t
 
   type t =
-    { entries : univ_entry LMap.t;
+    { entries : entry PMap.t;
       index : int;
       n_nodes : int; n_edges : int }
 
-  (** Used to cleanup universes if a traversal function is interrupted before it
-      has the opportunity to do it itself. *)
-  let unsafe_cleanup_universes g =
+  (** Used to cleanup mutable marks if a traversal function is
+      interrupted before it has the opportunity to do it itself. *)
+  let unsafe_cleanup_marks g =
     let iter _ n = match n with
       | Equiv _ -> ()
       | Canonical n -> n.status <- NoMark
     in
-    LMap.iter iter g.entries
+    PMap.iter iter g.entries
 
-  let rec cleanup_universes g =
-    try unsafe_cleanup_universes g
+  let rec cleanup_marks g =
+    try unsafe_cleanup_marks g
     with e ->
-      (* The only way unsafe_cleanup_universes may raise an exception is when
+      (* The only way unsafe_cleanup_marks may raise an exception is when
          a serious error (stack overflow, out of memory) occurs, or a signal is
          sent. In this unlikely event, we relaunch the cleanup until we finally
          succeed. *)
-      cleanup_universes g; raise e
+      cleanup_marks g; raise e
 
-  (* Every Level.t has a unique canonical arc representative *)
+  (* Every Point.t has a unique canonical arc representative *)
 
   (* Low-level function : makes u an alias for v.
      Does not removes edges from n_edges, but decrements n_nodes.
      u should be entered as canonical before.  *)
   let enter_equiv g u v =
     { entries =
-        LMap.modify u (fun _ a ->
+        PMap.modify u (fun _ a ->
             match a with
             | Canonical n ->
               n.status <- NoMark;
@@ -128,10 +128,10 @@ module Make (Level:Point) = struct
   (* Low-level function : changes data associated with a canonical node.
      Resets the mutable fields in the old record, in order to avoid breaking
      invariants for other users of this record.
-     n.univ should already been inserted as a canonical node. *)
+     n.canon should already been inserted as a canonical node. *)
   let change_node g n =
     { g with entries =
-               LMap.modify n.univ
+               PMap.modify n.canon
                  (fun _ a ->
                     match a with
                     | Canonical n' ->
@@ -140,21 +140,18 @@ module Make (Level:Point) = struct
                     | _ -> assert false)
                  g.entries }
 
-  (* repr : universes -> Level.t -> canonical_node *)
   (* canonical representative : we follow the Equiv links *)
   let rec repr g u =
-    let a =
-      try LMap.find u g.entries
-      with Not_found -> CErrors.anomaly ~label:"Univ.repr"
-                          Pp.(str"Universe " ++ Level.pr u ++ str" undefined.")
-    in
-    match a with
+    match PMap.find u g.entries with
     | Equiv v -> repr g v
     | Canonical arc -> arc
+    | exception Not_found ->
+      CErrors.anomaly ~label:"Univ.repr"
+        Pp.(str"Universe " ++ Point.pr u ++ str" undefined.")
 
   exception AlreadyDeclared
 
-  (* Reindexes the given universe, using the next available index. *)
+  (* Reindexes the given point, using the next available index. *)
   let use_index g u =
     let u = repr g u in
     let g = change_node g { u with ilvl = g.index } in
@@ -162,24 +159,24 @@ module Make (Level:Point) = struct
     { g with index = g.index - 1 }
 
   (* [safe_repr] is like [repr] but if the graph doesn't contain the
-     searched universe, we add it. *)
+     searched point, we add it. *)
   let safe_repr g u =
     let rec safe_repr_rec entries u =
-      match LMap.find u entries with
+      match PMap.find u entries with
       | Equiv v -> safe_repr_rec entries v
       | Canonical arc -> arc
     in
     try g, safe_repr_rec g.entries u
     with Not_found ->
       let can =
-        { univ = u;
-          ltle = LMap.empty; gtge = LSet.empty;
+        { canon = u;
+          ltle = PMap.empty; gtge = PSet.empty;
           rank = 0;
           klvl = 0; ilvl = 0;
           status = NoMark }
       in
       let g = { g with
-                entries = LMap.add u (Canonical can) g.entries;
+                entries = PMap.add u (Canonical can) g.entries;
                 n_nodes = g.n_nodes + 1 }
       in
       let g = use_index g u in
@@ -199,27 +196,27 @@ module Make (Level:Point) = struct
   let check_invariants ~required_canonical g =
     let n_edges = ref 0 in
     let n_nodes = ref 0 in
-    LMap.iter (fun l u ->
+    PMap.iter (fun l u ->
         match u with
         | Canonical u ->
-          LMap.iter (fun v _strict ->
+          PMap.iter (fun v _strict ->
               incr n_edges;
               let v = repr g v in
               assert (topo_compare u v = -1);
               if u.klvl = v.klvl then
-                assert (LSet.mem u.univ v.gtge ||
-                        LSet.exists (fun l -> u == repr g l) v.gtge))
+                assert (PSet.mem u.canon v.gtge ||
+                        PSet.exists (fun l -> u == repr g l) v.gtge))
             u.ltle;
-          LSet.iter (fun v ->
+          PSet.iter (fun v ->
               let v = repr g v in
               assert (v.klvl = u.klvl &&
-                      (LMap.mem u.univ v.ltle ||
-                       LMap.exists (fun l _ -> u == repr g l) v.ltle))
+                      (PMap.mem u.canon v.ltle ||
+                       PMap.exists (fun l _ -> u == repr g l) v.ltle))
             ) u.gtge;
           assert (u.status = NoMark);
-          assert (Level.equal l u.univ);
+          assert (Point.equal l u.canon);
           assert (u.ilvl > g.index);
-          assert (not (LMap.mem u.univ u.ltle));
+          assert (not (PMap.mem u.canon u.ltle));
           incr n_nodes
         | Equiv _ -> assert (not (required_canonical l)))
       g.entries;
@@ -227,20 +224,20 @@ module Make (Level:Point) = struct
     assert (!n_nodes = g.n_nodes)
 
   let clean_ltle g ltle =
-    LMap.fold (fun u strict acc ->
-        let uu = (repr g u).univ in
-        if Level.equal uu u then acc
+    PMap.fold (fun u strict acc ->
+        let uu = (repr g u).canon in
+        if Point.equal uu u then acc
         else (
-          let acc = LMap.remove u (fst acc) in
-          if not strict && LMap.mem uu acc then (acc, true)
-          else (LMap.add uu strict acc, true)))
+          let acc = PMap.remove u (fst acc) in
+          if not strict && PMap.mem uu acc then (acc, true)
+          else (PMap.add uu strict acc, true)))
       ltle (ltle, false)
 
   let clean_gtge g gtge =
-    LSet.fold (fun u acc ->
-        let uu = (repr g u).univ in
-        if Level.equal uu u then acc
-        else LSet.add uu (LSet.remove u (fst acc)), true)
+    PSet.fold (fun u acc ->
+        let uu = (repr g u).canon in
+        if Point.equal uu u then acc
+        else PSet.add uu (PSet.remove u (fst acc)), true)
       gtge (gtge, false)
 
   (* [get_ltle] and [get_gtge] return ltle and gtge arcs.
@@ -251,8 +248,8 @@ module Make (Level:Point) = struct
     let ltle, chgt_ltle = clean_ltle g u.ltle in
     if not chgt_ltle then u.ltle, u, g
     else
-      let sz = LMap.cardinal u.ltle in
-      let sz2 = LMap.cardinal ltle in
+      let sz = PMap.cardinal u.ltle in
+      let sz2 = PMap.cardinal ltle in
       let u = { u with ltle } in
       let g = change_node g u in
       let g = { g with n_edges = g.n_edges + sz2 - sz } in
@@ -271,7 +268,7 @@ module Make (Level:Point) = struct
      [to_revert] contains the touched nodes. *)
   let revert_graph to_revert g =
     List.iter (fun t ->
-        match LMap.find t g.entries with
+        match PMap.find t g.entries with
         | Equiv _ -> ()
         | Canonical t ->
           t.status <- NoMark) to_revert
@@ -305,14 +302,14 @@ module Make (Level:Point) = struct
     end;
     if x.status = NoMark then begin
       x.status <- Visited;
-      let to_revert = x.univ::to_revert in
+      let to_revert = x.canon::to_revert in
       let gtge, x, g = get_gtge g x in
       let to_revert, b_traversed, count, g =
-        LSet.fold (fun y (to_revert, b_traversed, count, g) ->
+        PSet.fold (fun y (to_revert, b_traversed, count, g) ->
             backward_traverse to_revert b_traversed count g y)
           gtge (to_revert, b_traversed, count, g)
       in
-      to_revert, x.univ::b_traversed, count, g
+      to_revert, x.canon::b_traversed, count, g
     end
     else to_revert, b_traversed, count, g
 
@@ -320,20 +317,20 @@ module Make (Level:Point) = struct
     let y = repr g y in
     if y.klvl < v_klvl then begin
       let y = { y with klvl = v_klvl;
-                       gtge = if x == y then LSet.empty
-                         else LSet.singleton x.univ }
+                       gtge = if x == y then PSet.empty
+                         else PSet.singleton x.canon }
       in
       let g = change_node g y in
       let ltle, y, g = get_ltle g y in
       let f_traversed, g =
-        LMap.fold (fun z _ (f_traversed, g) ->
+        PMap.fold (fun z _ (f_traversed, g) ->
             forward_traverse f_traversed g v_klvl y z)
           ltle (f_traversed, g)
       in
-      y.univ::f_traversed, g
+      y.canon::f_traversed, g
     end else if y.klvl = v_klvl && x != y then
       let g = change_node g
-          { y with gtge = LSet.add x.univ y.gtge } in
+          { y with gtge = PSet.add x.canon y.gtge } in
       f_traversed, g
     else f_traversed, g
 
@@ -343,11 +340,11 @@ module Make (Level:Point) = struct
     | Visited -> false, to_revert   | ToMerge -> true, to_revert
     | NoMark ->
       let to_revert = x::to_revert in
-      if Level.equal x.univ v then
+      if Point.equal x.canon v then
         begin x.status <- ToMerge; true, to_revert end
       else
         begin
-          let merge, to_revert = LSet.fold
+          let merge, to_revert = PSet.fold
               (fun y (merge, to_revert) ->
                  let merge', to_revert = find_to_merge to_revert g y v in
                  merge' || merge, to_revert) x.gtge (false, to_revert)
@@ -360,23 +357,23 @@ module Make (Level:Point) = struct
   let get_new_edges g to_merge =
     (* Computing edge sets. *)
     let to_merge_lvl =
-      List.fold_left (fun acc u -> LMap.add u.univ u acc)
-        LMap.empty to_merge
+      List.fold_left (fun acc u -> PMap.add u.canon u acc)
+        PMap.empty to_merge
     in
     let ltle =
       let fold _ n acc =
         let fold u strict acc =
-          if strict then LMap.add u strict acc
-          else if LMap.mem u acc then acc
-          else LMap.add u false acc
+          if strict then PMap.add u strict acc
+          else if PMap.mem u acc then acc
+          else PMap.add u false acc
         in
-        LMap.fold fold n.ltle acc
+        PMap.fold fold n.ltle acc
       in
-      LMap.fold fold to_merge_lvl LMap.empty
+      PMap.fold fold to_merge_lvl PMap.empty
     in
     let ltle, _ = clean_ltle g ltle in
     let ltle =
-      LMap.merge (fun _ a strict ->
+      PMap.merge (fun _ a strict ->
           match a, strict with
           | Some _, Some true ->
             (* There is a lt edge inside the new component. This is a
@@ -387,11 +384,11 @@ module Make (Level:Point) = struct
         ) to_merge_lvl ltle
     in
     let gtge =
-      LMap.fold (fun _ n acc -> LSet.union acc n.gtge)
-        to_merge_lvl LSet.empty
+      PMap.fold (fun _ n acc -> PSet.union acc n.gtge)
+        to_merge_lvl PSet.empty
     in
     let gtge, _ = clean_gtge g gtge in
-    let gtge = LSet.diff gtge (LMap.domain to_merge_lvl) in
+    let gtge = PSet.diff gtge (PMap.domain to_merge_lvl) in
     (ltle, gtge)
 
 
@@ -456,21 +453,21 @@ module Make (Level:Point) = struct
 
         (* Inserting shortcuts for old nodes. *)
         let g = List.fold_left (fun g n ->
-            if Level.equal n.univ root.univ then g else enter_equiv g n.univ root.univ)
+            if Point.equal n.canon root.canon then g else enter_equiv g n.canon root.canon)
             g to_merge
         in
 
         (* Updating g.n_edges *)
         let oldsz =
-          List.fold_left (fun sz u -> sz+LMap.cardinal u.ltle)
+          List.fold_left (fun sz u -> sz+PMap.cardinal u.ltle)
             0 to_merge
         in
-        let sz = LMap.cardinal ltle in
+        let sz = PMap.cardinal ltle in
         let g = { g with n_edges = g.n_edges + sz - oldsz } in
 
         (* Not clear in the paper: we have to put the newly
             created component just between B and F. *)
-        List.rev_append f_reindex (root.univ::b_reindex), g
+        List.rev_append f_reindex (root.canon::b_reindex), g
 
     in
 
@@ -481,7 +478,7 @@ module Make (Level:Point) = struct
   (* Does NOT assume that ucan != vcan. *)
   let insert_edge strict ucan vcan g =
     try
-      let u = ucan.univ and v = vcan.univ in
+      let u = ucan.canon and v = vcan.canon in
       (* STEP 1: do we need to reorder nodes ? *)
       let g = if topo_compare ucan vcan <= 0 then g else reorder g u v in
 
@@ -492,68 +489,68 @@ module Make (Level:Point) = struct
         if strict then raise CycleDetected else g
       else
         let g =
-          try let oldstrict = LMap.find v.univ u.ltle in
+          try let oldstrict = PMap.find v.canon u.ltle in
             if strict && not oldstrict then
-              change_node g { u with ltle = LMap.add v.univ true u.ltle }
+              change_node g { u with ltle = PMap.add v.canon true u.ltle }
             else g
           with Not_found ->
-            { (change_node g { u with ltle = LMap.add v.univ strict u.ltle })
+            { (change_node g { u with ltle = PMap.add v.canon strict u.ltle })
               with n_edges = g.n_edges + 1 }
         in
-        if u.klvl <> v.klvl || LSet.mem u.univ v.gtge then g
+        if u.klvl <> v.klvl || PSet.mem u.canon v.gtge then g
         else
-          let v = { v with gtge = LSet.add u.univ v.gtge } in
+          let v = { v with gtge = PSet.add u.canon v.gtge } in
           change_node g v
     with
     | CycleDetected as e -> raise e
     | e ->
       (* Unlikely event: fatal error or signal *)
-      let () = cleanup_universes g in
+      let () = cleanup_marks g in
       raise e
 
-  let add ?(rank=0) vlev g =
+  let add ?(rank=0) v g =
     try
-      let _arcv = LMap.find vlev g.entries in
+      let _arcv = PMap.find v g.entries in
       raise AlreadyDeclared
     with Not_found ->
       assert (g.index > min_int);
-      let v = {
-        univ = vlev;
-        ltle = LMap.empty;
-        gtge = LSet.empty;
+      let node = {
+        canon = v;
+        ltle = PMap.empty;
+        gtge = PSet.empty;
         rank;
         klvl = 0;
         ilvl = g.index;
         status = NoMark;
       }
       in
-      let entries = LMap.add vlev (Canonical v) g.entries in
+      let entries = PMap.add v (Canonical node) g.entries in
       { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges }
 
-  exception Undeclared of Level.t
+  exception Undeclared of Point.t
   let check_declared g us =
-    let check l = if not (LMap.mem l g.entries) then raise (Undeclared l) in
-    LSet.iter check us
+    let check l = if not (PMap.mem l g.entries) then raise (Undeclared l) in
+    PSet.iter check us
 
-  exception Found_explanation of (constraint_type * Level.t) list
+  exception Found_explanation of (constraint_type * Point.t) list
 
   let get_explanation strict u v g =
     let v = repr g v in
-    let visited_strict = ref LMap.empty in
+    let visited_strict = ref PMap.empty in
     let rec traverse strict u =
       if u == v then
         if strict then None else Some []
       else if topo_compare u v = 1 then None
       else
         let visited =
-          try not (LMap.find u.univ !visited_strict) || strict
+          try not (PMap.find u.canon !visited_strict) || strict
           with Not_found -> false
         in
         if visited then None
         else begin
-          visited_strict := LMap.add u.univ strict !visited_strict;
+          visited_strict := PMap.add u.canon strict !visited_strict;
           try
-            LMap.iter (fun u' strictu' ->
+            PMap.iter (fun u' strictu' ->
                 match traverse (strict && not strictu') (repr g u') with
                 | None -> ()
                 | Some exp ->
@@ -565,7 +562,7 @@ module Make (Level:Point) = struct
         end
     in
     let u = repr g u in
-    if u == v then [(Eq, v.univ)]
+    if u == v then [(Eq, v.canon)]
     else match traverse strict u with Some exp -> exp | None -> assert false
 
   let get_explanation strict u v g =
@@ -591,13 +588,13 @@ module Make (Level:Point) = struct
             if u.status = NoMark then u::to_revert else to_revert
           in
           u.status <- if strict then WeakVisited else Visited;
-          if try LMap.find v.univ u.ltle || not strict
+          if try PMap.find v.canon u.ltle || not strict
             with Not_found -> false
           then raise (Found to_revert)
           else
             begin
               let next_todo =
-                LMap.fold (fun u strictu next_todo ->
+                PMap.fold (fun u strictu next_todo ->
                     let strict = not strictu && strict in
                     let u = repr g u in
                     if u == v && not strict then raise (Found to_revert)
@@ -619,7 +616,7 @@ module Make (Level:Point) = struct
         res
       with e ->
         (* Unlikely event: fatal error or signal *)
-        let () = cleanup_universes g in
+        let () = cleanup_marks g in
         raise e
 
   (** Uncomment to debug the cycle detection algorithm. *)
@@ -628,12 +625,12 @@ module Make (Level:Point) = struct
     check_invariants g;
     let g = insert_edge strict ucan vcan g in
     check_invariants g;
-    let ucan = repr g ucan.univ in
-    let vcan = repr g vcan.univ in
+    let ucan = repr g ucan.canon in
+    let vcan = repr g vcan.canon in
     assert (search_path strict ucan vcan g);
     g*)
 
-  (** First, checks on universe levels *)
+  (** User interface *)
 
   type 'a check_function = t -> 'a -> 'a -> bool
 
@@ -658,7 +655,7 @@ module Make (Level:Point) = struct
       let g = insert_edge false ucan vcan g in  (* Cannot fail *)
       try insert_edge false vcan ucan g
       with CycleDetected ->
-        Level.error_inconsistency Eq v u (get_explanation true u v g)
+        Point.error_inconsistency Eq v u (get_explanation true u v g)
 
   (* enforce_leq g u v will force u<=v if possible, will fail otherwise *)
   let enforce_leq u v g =
@@ -666,7 +663,7 @@ module Make (Level:Point) = struct
     let vcan = repr g v in
     try insert_edge false ucan vcan g
     with CycleDetected ->
-      Level.error_inconsistency Le u v (get_explanation true v u g)
+      Point.error_inconsistency Le u v (get_explanation true v u g)
 
   (* enforce_lt u v will force u<v if possible, will fail otherwise *)
   let enforce_lt u v g =
@@ -674,28 +671,28 @@ module Make (Level:Point) = struct
     let vcan = repr g v in
     try insert_edge true ucan vcan g
     with CycleDetected ->
-      Level.error_inconsistency Lt u v (get_explanation false v u g)
+      Point.error_inconsistency Lt u v (get_explanation false v u g)
 
   let empty =
-    { entries = LMap.empty; index = 0; n_nodes = 0; n_edges = 0 }
+    { entries = PMap.empty; index = 0; n_nodes = 0; n_edges = 0 }
 
   (* Normalization *)
 
-  (** [normalize_universes g] returns a graph where all edges point
+  (** [normalize g] returns a graph where all edges point
       directly to the canonical representent of their target. The output
       graph should be equivalent to the input graph from a logical point
       of view, but optimized. We maintain the invariant that the key of
       a [Canonical] element is its own name, by keeping [Equiv] edges. *)
-  let normalize_universes g =
+  let normalize g =
     let g =
       { g with
-        entries = LMap.map (fun entry ->
+        entries = PMap.map (fun entry ->
             match entry with
-            | Equiv u -> Equiv ((repr g u).univ)
+            | Equiv u -> Equiv ((repr g u).canon)
             | Canonical ucan -> Canonical { ucan with rank = 1 })
             g.entries }
     in
-    LMap.fold (fun _ u g ->
+    PMap.fold (fun _ u g ->
         match u with
         | Equiv _u -> g
         | Canonical u ->
@@ -705,108 +702,100 @@ module Make (Level:Point) = struct
       g.entries g
 
   let constraints_of g =
-    let module UF = Unionfind.Make (LSet) (LMap) in
+    let module UF = Unionfind.Make (PSet) (PMap) in
     let uf = UF.create () in
     let constraints_of u v acc =
       match v with
-      | Canonical {univ=u; ltle; _} ->
-        LMap.fold (fun v strict acc->
+      | Canonical {canon=u; ltle; _} ->
+        PMap.fold (fun v strict acc->
             let typ = if strict then Lt else Le in
             Constraint.add (u,typ,v) acc) ltle acc
       | Equiv v -> UF.union u v uf; acc
     in
-    let csts = LMap.fold constraints_of g.entries Constraint.empty in
+    let csts = PMap.fold constraints_of g.entries Constraint.empty in
     csts, UF.partition uf
 
   (* domain g.entries = kept + removed *)
   let constraints_for ~kept g =
-    (* rmap: partial map from canonical universes to kept universes *)
-    let rmap, csts = LSet.fold (fun u (rmap,csts) ->
+    (* rmap: partial map from canonical points to kept points *)
+    let rmap, csts = PSet.fold (fun u (rmap,csts) ->
         let arcu = repr g u in
-        if LSet.mem arcu.univ kept then
-          LMap.add arcu.univ arcu.univ rmap, Constraint.add (u,Eq,arcu.univ) csts
+        if PSet.mem arcu.canon kept then
+          PMap.add arcu.canon arcu.canon rmap, Constraint.add (u,Eq,arcu.canon) csts
         else
-          match LMap.find arcu.univ rmap with
+          match PMap.find arcu.canon rmap with
           | v -> rmap, Constraint.add (u,Eq,v) csts
-          | exception Not_found -> LMap.add arcu.univ u rmap, csts)
-        kept (LMap.empty,Constraint.empty)
+          | exception Not_found -> PMap.add arcu.canon u rmap, csts)
+        kept (PMap.empty,Constraint.empty)
     in
     let rec add_from u csts todo = match todo with
       | [] -> csts
       | (v,strict)::todo ->
         let v = repr g v in
-        (match LMap.find v.univ rmap with
+        (match PMap.find v.canon rmap with
          | v ->
            let d = if strict then Lt else Le in
            let csts = Constraint.add (u,d,v) csts in
            add_from u csts todo
          | exception Not_found ->
-           (* v is not equal to any kept universe *)
-           let todo = LMap.fold (fun v' strict' todo ->
+           (* v is not equal to any kept point *)
+           let todo = PMap.fold (fun v' strict' todo ->
                (v',strict || strict') :: todo)
                v.ltle todo
            in
            add_from u csts todo)
     in
-    LSet.fold (fun u csts ->
+    PSet.fold (fun u csts ->
         let arc = repr g u in
-        LMap.fold (fun v strict csts -> add_from u csts [v,strict])
+        PMap.fold (fun v strict csts -> add_from u csts [v,strict])
           arc.ltle csts)
       kept csts
 
-  let domain g = LMap.domain g.entries
+  let domain g = PMap.domain g.entries
 
   let choose p g u =
-    let exception Found of Level.t in
-    let ru = (repr g u).univ in
+    let exception Found of Point.t in
+    let ru = (repr g u).canon in
     if p ru then Some ru
     else
-      try LMap.iter (fun v -> function
+      try PMap.iter (fun v -> function
           | Canonical _ -> () (* we already tried [p ru] *)
           | Equiv v' ->
-            let rv = (repr g v').univ in
+            let rv = (repr g v').canon in
             if rv == ru && p v then raise (Found v)
             (* NB: we could also try [p v'] but it will come up in the
                rest of the iteration regardless. *)
         ) g.entries; None
       with Found v -> Some v
 
-  (** [sort_universes g] builds a totally ordered universe graph.  The
-      output graph should imply the input graph (and the implication
-      will be strict most of the time), but is not necessarily minimal.
-      Moreover, it adds levels [Type.n] to identify universes at level
-      n. An artificial constraint Set < Type.2 is added to ensure that
-      Type.n and small universes are not merged. Note: the result is
-      unspecified if the input graph already contains [Type.n] nodes
-      (calling a module Type is probably a bad idea anyway). *)
-  let sort make_dummy univs g =
+  let sort make_dummy first g =
     let cans =
-      LMap.fold (fun _ u l ->
+      PMap.fold (fun _ u l ->
           match u with
           | Equiv _ -> l
           | Canonical can -> can :: l
         ) g.entries []
     in
     let cans = List.sort topo_compare cans in
-    let lowest_levels =
-      LMap.mapi (fun u _ -> if CList.mem_f Level.equal u univs then 0 else 2)
-        (LMap.filter
+    let lowest =
+      PMap.mapi (fun u _ -> if CList.mem_f Point.equal u first then 0 else 2)
+        (PMap.filter
            (fun _ u -> match u with Equiv _ -> false | Canonical _ -> true)
            g.entries)
     in
-    let lowest_levels =
-      List.fold_left (fun lowest_levels can ->
-          let lvl = LMap.find can.univ lowest_levels in
-          LMap.fold (fun u' strict lowest_levels ->
+    let lowest =
+      List.fold_left (fun lowest can ->
+          let lvl = PMap.find can.canon lowest in
+          PMap.fold (fun u' strict lowest ->
               let cost = if strict then 1 else 0 in
-              let u' = (repr g u').univ in
-              LMap.modify u' (fun _ lvl0 -> max lvl0 (lvl+cost)) lowest_levels)
-            can.ltle lowest_levels)
-        lowest_levels cans
+              let u' = (repr g u').canon in
+              PMap.modify u' (fun _ lvl0 -> max lvl0 (lvl+cost)) lowest)
+            can.ltle lowest)
+        lowest cans
     in
-    let max_lvl = LMap.fold (fun _ a b -> max a b) lowest_levels 0 in
+    let max_lvl = PMap.fold (fun _ a b -> max a b) lowest 0 in
     let types = Array.init (max_lvl + 1) (fun i ->
-        match List.nth_opt univs i with
+        match List.nth_opt first i with
         | Some u -> u
         | None -> make_dummy (i-2))
     in
@@ -814,30 +803,30 @@ module Make (Level:Point) = struct
         let g, u = safe_repr g u in
         change_node g { u with rank = big_rank }) g types
     in
-    let g = if max_lvl > List.length univs && not (CList.is_empty univs) then
-        enforce_lt (CList.last univs) types.(List.length univs) g
+    let g = if max_lvl > List.length first && not (CList.is_empty first) then
+        enforce_lt (CList.last first) types.(List.length first) g
       else g
     in
     let g =
-      LMap.fold (fun u lvl g -> enforce_eq u (types.(lvl)) g)
-        lowest_levels g
+      PMap.fold (fun u lvl g -> enforce_eq u (types.(lvl)) g)
+        lowest g
     in
-    normalize_universes g
+    normalize g
 
   (** Pretty-printing *)
 
-  let pr_umap sep pr map =
-    let cmp (u,_) (v,_) = Level.compare u v in
-    Pp.prlist_with_sep sep pr (List.sort cmp (LMap.bindings map))
+  let pr_pmap sep pr map =
+    let cmp (u,_) (v,_) = Point.compare u v in
+    Pp.prlist_with_sep sep pr (List.sort cmp (PMap.bindings map))
 
   let pr_arc prl = let open Pp in
     function
-    | _, Canonical {univ=u; ltle; _} ->
-      if LMap.is_empty ltle then mt ()
+    | _, Canonical {canon=u; ltle; _} ->
+      if PMap.is_empty ltle then mt ()
       else
         prl u ++ str " " ++
         v 0
-          (pr_umap spc (fun (v, strict) ->
+          (pr_pmap spc (fun (v, strict) ->
                (if strict then str "< " else str "<= ") ++ prl v)
               ltle) ++
         fnl ()
@@ -845,19 +834,19 @@ module Make (Level:Point) = struct
       prl u  ++ str " = " ++ prl v ++ fnl ()
 
   let pr prl g =
-    pr_umap Pp.mt (pr_arc prl) g.entries
+    pr_pmap Pp.mt (pr_arc prl) g.entries
 
   (* Dumping constraints to a file *)
 
   let dump output g =
     let dump_arc u = function
-      | Canonical {univ=u; ltle; _} ->
-        LMap.iter (fun v strict ->
+      | Canonical {canon=u; ltle; _} ->
+        PMap.iter (fun v strict ->
             let typ = if strict then Lt else Le in
             output typ u v) ltle;
       | Equiv v ->
         output Eq u v
     in
-    LMap.iter dump_arc g.entries
+    PMap.iter dump_arc g.entries
 
 end
diff --git a/lib/acyclicGraph.mli b/lib/acyclicGraph.mli
index 8a2eb7098f..13a12b51cd 100644
--- a/lib/acyclicGraph.mli
+++ b/lib/acyclicGraph.mli
@@ -29,45 +29,51 @@ module type Point = sig
   val pr : t -> Pp.t
 end
 
-module Make (Level:Point) : sig
+module Make (Point:Point) : sig
 
   type t
 
   val empty : t
 
-  val check_invariants : required_canonical:(Level.t -> bool) -> t -> unit
+  val check_invariants : required_canonical:(Point.t -> bool) -> t -> unit
 
   exception AlreadyDeclared
-  val add : ?rank:int -> Level.t -> t -> t
+  val add : ?rank:int -> Point.t -> t -> t
   (** Use a large [rank] to keep the node canonical *)
 
-  exception Undeclared of Level.t
-  val check_declared : t -> Level.Set.t -> unit
+  exception Undeclared of Point.t
+  val check_declared : t -> Point.Set.t -> unit
 
   type 'a check_function = t -> 'a -> 'a -> bool
 
-  val check_eq : Level.t check_function
-  val check_leq : Level.t check_function
-  val check_lt : Level.t check_function
+  val check_eq : Point.t check_function
+  val check_leq : Point.t check_function
+  val check_lt : Point.t check_function
 
-  val enforce_eq : Level.t -> Level.t -> t -> t
-  val enforce_leq : Level.t -> Level.t -> t -> t
-  val enforce_lt : Level.t -> Level.t -> t -> t
+  val enforce_eq : Point.t -> Point.t -> t -> t
+  val enforce_leq : Point.t -> Point.t -> t -> t
+  val enforce_lt : Point.t -> Point.t -> t -> t
 
-  val constraints_of : t -> Level.Constraint.t * Level.Set.t list
+  val constraints_of : t -> Point.Constraint.t * Point.Set.t list
 
-  val constraints_for : kept:Level.Set.t -> t -> Level.Constraint.t
+  val constraints_for : kept:Point.Set.t -> t -> Point.Constraint.t
 
-  val domain : t -> Level.Set.t
+  val domain : t -> Point.Set.t
 
-  val choose : (Level.t -> bool) -> t -> Level.t -> Level.t option
+  val choose : (Point.t -> bool) -> t -> Point.t -> Point.t option
 
-  val sort : (int -> Level.t) -> Level.t list -> t -> t
-  (** [sort make_dummy points g] sorts [g]. The [points] are the first
-     in the result graph. If the graph is bigger than the list, the
-     rest is named according to [make_dummy]. *)
+  val sort : (int -> Point.t) -> Point.t list -> t -> t
+  (** [sort mk first g] builds a totally ordered graph. The output
+     graph should imply the input graph (and the implication will be
+     strict most of the time), but is not necessarily minimal. The
+     lowest points in the result are identified with [first].
+     Moreover, it adds levels [Type.n] to identify the points (not in
+     [first]) at level n. An artificial constraint (last first < mk
+     (length first)) is added to ensure that they are not merged.
+     Note: the result is unspecified if the input graph already
+     contains [mk n] nodes. *)
 
-  val pr : (Level.t -> Pp.t) -> t -> Pp.t
+  val pr : (Point.t -> Pp.t) -> t -> Pp.t
 
-  val dump : (constraint_type -> Level.t -> Level.t -> unit) -> t -> unit
+  val dump : (constraint_type -> Point.t -> Point.t -> unit) -> t -> unit
 end