Splitting kernel universe code in two modules.

1. The Univ module now only cares about definitions about universes.
2. The UGraph module contains the algorithm responsible for aciclicity.

27 files changed, 1034 insertions, 977 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 07b48ed57..f19edf1c8 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -55,6 +55,7 @@ Monad
 
 Names
 Univ
+UGraph
 Esubst
 Uint31
 Sorts
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 0900bb096..1d3d711ac 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -221,7 +221,7 @@ let ppuniverseconstraints c = pp (Universes.Constraints.pr c)
 let ppuniverse_context_future c = 
   let ctx = Future.force c in
     ppuniverse_context ctx
-let ppuniverses u = pp (Univ.pr_universes Level.pr u)
+let ppuniverses u = pp (UGraph.pr_universes Level.pr u)
 let ppnamedcontextval e =
   pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e))
 
diff --git a/engine/evd.ml b/engine/evd.ml
index cd0b52eca..3f4bfe7af 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -283,8 +283,8 @@ type evar_universe_context =
    (** The subset of unification variables that
 	can be instantiated with algebraic universes as they appear in types 
 	and universe instances only. *)
-   uctx_universes : Univ.universes; (** The current graph extended with the local constraints *)
-   uctx_initial_universes : Univ.universes; (** The graph at the creation of the evar_map *)
+   uctx_universes : UGraph.t; (** The current graph extended with the local constraints *)
+   uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *)
  }
   
 let empty_evar_universe_context = 
@@ -292,8 +292,8 @@ let empty_evar_universe_context =
     uctx_local = Univ.ContextSet.empty;
     uctx_univ_variables = Univ.LMap.empty;
     uctx_univ_algebraic = Univ.LSet.empty;
-    uctx_universes = Univ.initial_universes;
-    uctx_initial_universes = Univ.initial_universes }
+    uctx_universes = UGraph.initial_universes;
+    uctx_initial_universes = UGraph.initial_universes }
 
 let evar_universe_context_from e = 
   let u = universes e in
@@ -314,7 +314,7 @@ let union_evar_universe_context ctx ctx' =
 			       (Univ.ContextSet.levels ctx.uctx_local) in
     let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in
     let declarenew g =
-      Univ.LSet.fold (fun u g -> Univ.add_universe u false g) newus g
+      Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) newus g
     in
     let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in
       { uctx_names = (names, names_rev);
@@ -328,7 +328,7 @@ let union_evar_universe_context ctx ctx' =
 	  if local == ctx.uctx_local then ctx.uctx_universes
 	  else
 	    let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in
-	      Univ.merge_constraints cstrsr (declarenew ctx.uctx_universes) }
+	      UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes) }
 
 (* let union_evar_universe_context_key = Profile.declare_profile "union_evar_universe_context";; *)
 (* let union_evar_universe_context =  *)
@@ -374,7 +374,7 @@ let process_universe_constraints univs vars alg cstrs =
 	  | Some l -> Inr (l, Univ.LMap.mem l !vars, Univ.LSet.mem l alg)
 	in
 	  if d == Universes.ULe then
-	    if Univ.check_leq univs l r then
+	    if UGraph.check_leq univs l r then
 	      (** Keep Prop/Set <= var around if var might be instantiated by prop or set
 		  later. *)
 	      if Univ.Universe.is_level l then 
@@ -413,7 +413,7 @@ let process_universe_constraints univs vars alg cstrs =
 		  instantiate_variable l' r vars
 		else if rloc then 
 		  instantiate_variable r' l vars
-		else if not (Univ.check_eq univs l r) then
+		else if not (UGraph.check_eq univs l r) then
 		  (* Two rigid/global levels, none of them being local,
 		     one of them being Prop/Set, disallow *)
 		  if Univ.Level.is_small l' || Univ.Level.is_small r' then
@@ -433,7 +433,7 @@ let process_universe_constraints univs vars alg cstrs =
 		     Univ.enforce_leq inst lu local
 		   else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None))
             | _, _ (* One of the two is algebraic or global *) -> 
-	     if Univ.check_eq univs l r then local
+	     if UGraph.check_eq univs l r then local
 	     else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
   in
   let local = 
@@ -459,7 +459,7 @@ let add_constraints_context ctx cstrs =
   in
     { ctx with uctx_local = (univs, Univ.Constraint.union local local');
       uctx_univ_variables = vars;
-      uctx_universes = Univ.merge_constraints local' ctx.uctx_universes }
+      uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes }
 
 (* let addconstrkey = Profile.declare_profile "add_constraints_context";; *)
 (* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *)
@@ -473,7 +473,7 @@ let add_universe_constraints_context ctx cstrs =
   in
     { ctx with uctx_local = (univs, Univ.Constraint.union local local');
       uctx_univ_variables = vars;
-      uctx_universes = Univ.merge_constraints local' ctx.uctx_universes }
+      uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes }
 
 (* let addunivconstrkey = Profile.declare_profile "add_universe_constraints_context";; *)
 (* let add_universe_constraints_context =  *)
@@ -1012,13 +1012,13 @@ let merge_uctx sideff rigid uctx ctx' =
   in
   let declare g =
     LSet.fold (fun u g ->
-	       try Univ.add_universe u false g
-	       with Univ.AlreadyDeclared when sideff -> g)
+	       try UGraph.add_universe u false g
+	       with UGraph.AlreadyDeclared when sideff -> g)
 	      levels g
   in
   let initial = declare uctx.uctx_initial_universes in
   let univs = declare uctx.uctx_universes in
-  let uctx_universes = merge_constraints (ContextSet.constraints ctx') univs in
+  let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in
     { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial }
 
 let merge_context_set rigid evd ctx' = 
@@ -1079,11 +1079,11 @@ let uctx_new_univ_variable rigid name predicative
     | None -> uctx.uctx_names
   in
   let initial =
-    Univ.add_universe u false uctx.uctx_initial_universes
+    UGraph.add_universe u false uctx.uctx_initial_universes
   in						     
   let uctx' =
     {uctx' with uctx_names = names; uctx_local = ctx';
-		uctx_universes = Univ.add_universe u false uctx.uctx_universes;
+		uctx_universes = UGraph.add_universe u false uctx.uctx_universes;
 		uctx_initial_universes = initial}
   in uctx', u
 						     
@@ -1102,10 +1102,10 @@ let new_sort_variable ?name ?(predicative=true) rigid d =
 let add_global_univ d u =
   let uctx = d.universes in
   let initial =
-    Univ.add_universe u true uctx.uctx_initial_universes
+    UGraph.add_universe u true uctx.uctx_initial_universes
   in
   let univs = 
-    Univ.add_universe u true uctx.uctx_universes
+    UGraph.add_universe u true uctx.uctx_universes
   in
     { d with universes = { uctx with uctx_local = Univ.ContextSet.add_universe u uctx.uctx_local;
 				     uctx_initial_universes = initial;
@@ -1245,10 +1245,10 @@ let set_leq_sort env evd s1 s2 =
       else evd
 	    
 let check_eq evd s s' =
-  Univ.check_eq evd.universes.uctx_universes s s'
+  UGraph.check_eq evd.universes.uctx_universes s s'
 
 let check_leq evd s s' =
-  Univ.check_leq evd.universes.uctx_universes s s'
+  UGraph.check_leq evd.universes.uctx_universes s s'
 
 let subst_univs_context_with_def def usubst (ctx, cst) =
   (Univ.LSet.diff ctx def, Univ.subst_univs_constraints usubst cst)
@@ -1301,10 +1301,10 @@ let refresh_undefined_univ_variables uctx =
           (Option.map (Univ.subst_univs_level_universe subst) v) acc)
       uctx.uctx_univ_variables Univ.LMap.empty
   in
-  let declare g = Univ.LSet.fold (fun u g -> Univ.add_universe u false g)
+  let declare g = Univ.LSet.fold (fun u g -> UGraph.add_universe u false g)
 				   (Univ.ContextSet.levels ctx') g in
   let initial = declare uctx.uctx_initial_universes in
-  let univs = declare Univ.initial_universes in
+  let univs = declare UGraph.initial_universes in
   let uctx' = {uctx_names = uctx.uctx_names;
 	       uctx_local = ctx'; 
 	       uctx_univ_variables = vars; uctx_univ_algebraic = alg;
diff --git a/engine/evd.mli b/engine/evd.mli
index db60f5ff4..22d017497 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -489,7 +489,7 @@ val restrict_universe_context : evar_map -> Univ.universe_set -> evar_map
 val universe_of_name : evar_map -> string -> Univ.universe_level
 val add_universe_name : evar_map -> string -> Univ.universe_level -> evar_map
 
-val universes : evar_map -> Univ.universes
+val universes : evar_map -> UGraph.t
 
 val add_constraints_context : evar_universe_context -> 
   Univ.constraints -> evar_universe_context
@@ -532,7 +532,7 @@ val evar_universe_context : evar_map -> evar_universe_context
 val universe_context_set : evar_map -> Univ.universe_context_set
 val universe_context : ?names:(Id.t located) list -> evar_map -> Univ.universe_context
 val universe_subst : evar_map -> Universes.universe_opt_subst
-val universes : evar_map -> Univ.universes
+val universes : evar_map -> UGraph.t
 
 
 val merge_universe_context : evar_map -> evar_universe_context -> evar_map
diff --git a/kernel/constr.ml b/kernel/constr.ml
index e2b1d3fd9..753d18845 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -545,8 +545,8 @@ let equal m n = eq_constr m n (* to avoid tracing a recursive fun *)
 let eq_constr_univs univs m n =
   if m == n then true
   else 
-    let eq_universes _ = Univ.Instance.check_eq univs in
-    let eq_sorts s1 s2 = s1 == s2 || Univ.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in
+    let eq_universes _ = UGraph.check_eq_instances univs in
+    let eq_sorts s1 s2 = s1 == s2 || UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in
     let rec eq_constr' m n = 
       m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
     in compare_head_gen eq_universes eq_sorts eq_constr' m n
@@ -554,11 +554,11 @@ let eq_constr_univs univs m n =
 let leq_constr_univs univs m n =
   if m == n then true
   else 
-    let eq_universes _ = Univ.Instance.check_eq univs in
+    let eq_universes _ = UGraph.check_eq_instances univs in
     let eq_sorts s1 s2 = s1 == s2 || 
-      Univ.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in
+      UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in
     let leq_sorts s1 s2 = s1 == s2 || 
-      Univ.check_leq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in
+      UGraph.check_leq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in
     let rec eq_constr' m n = 
       m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
     in
@@ -571,12 +571,12 @@ let eq_constr_univs_infer univs m n =
   if m == n then true, Constraint.empty
   else 
     let cstrs = ref Constraint.empty in
-    let eq_universes strict = Univ.Instance.check_eq univs in
+    let eq_universes strict = UGraph.check_eq_instances univs in
     let eq_sorts s1 s2 = 
       if Sorts.equal s1 s2 then true
       else
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	if Univ.check_eq univs u1 u2 then true
+	if UGraph.check_eq univs u1 u2 then true
 	else
 	  (cstrs := Univ.enforce_eq u1 u2 !cstrs;
 	   true)
@@ -591,12 +591,12 @@ let leq_constr_univs_infer univs m n =
   if m == n then true, Constraint.empty
   else 
     let cstrs = ref Constraint.empty in
-    let eq_universes strict l l' = Univ.Instance.check_eq univs l l' in
+    let eq_universes strict l l' = UGraph.check_eq_instances univs l l' in
     let eq_sorts s1 s2 = 
       if Sorts.equal s1 s2 then true
       else
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	if Univ.check_eq univs u1 u2 then true
+	if UGraph.check_eq univs u1 u2 then true
 	else (cstrs := Univ.enforce_eq u1 u2 !cstrs;
 	      true)
     in
@@ -604,7 +604,7 @@ let leq_constr_univs_infer univs m n =
       if Sorts.equal s1 s2 then true
       else 
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	if Univ.check_leq univs u1 u2 then true
+	if UGraph.check_leq univs u1 u2 then true
 	else
 	  (cstrs := Univ.enforce_leq u1 u2 !cstrs; 
 	   true)
diff --git a/kernel/constr.mli b/kernel/constr.mli
index e6a3e71f8..5a370d31d 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -205,19 +205,19 @@ val equal : constr -> constr -> bool
 
 (** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts,
    application grouping and the universe equalities in [u]. *)
-val eq_constr_univs : constr Univ.check_function
+val eq_constr_univs : constr UGraph.check_function
 
 (** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo 
     alpha, casts, application grouping and the universe inequalities in [u]. *)
-val leq_constr_univs : constr Univ.check_function
+val leq_constr_univs : constr UGraph.check_function
 
 (** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts,
    application grouping and the universe equalities in [u]. *)
-val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.constrained
+val eq_constr_univs_infer : UGraph.t -> constr -> constr -> bool Univ.constrained
 
 (** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo 
     alpha, casts, application grouping and the universe inequalities in [u]. *)
-val leq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.constrained
+val leq_constr_univs_infer : UGraph.t -> constr -> constr -> bool Univ.constrained
 
 (** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts,
    application grouping and ignoring universe instances. *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 1cc07c0ab..09fe64d77 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -188,10 +188,10 @@ let map_universes f env =
 				     
 let add_constraints c env =
   if Univ.Constraint.is_empty c then env
-  else map_universes (Univ.merge_constraints c) env
+  else map_universes (UGraph.merge_constraints c) env
 
 let check_constraints c env =
-  Univ.check_constraints c env.env_stratification.env_universes
+  UGraph.check_constraints c env.env_stratification.env_universes
 
 let push_constraints_to_env (_,univs) env =
   add_constraints univs env
@@ -199,19 +199,19 @@ let push_constraints_to_env (_,univs) env =
 let add_universes strict ctx g =
   let g = Array.fold_left
 	    (* Be lenient, module typing reintroduces universes and constraints due to includes *)
-	    (fun g v -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g)
+	    (fun g v -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g)
 	    g (Univ.Instance.to_array (Univ.UContext.instance ctx))
   in
-    Univ.merge_constraints (Univ.UContext.constraints ctx) g
+    UGraph.merge_constraints (Univ.UContext.constraints ctx) g
 			   
 let push_context ?(strict=false) ctx env =
   map_universes (add_universes strict ctx) env
 
 let add_universes_set strict ctx g =
   let g = Univ.LSet.fold
-	    (fun v g -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g)
+	    (fun v g -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g)
 	    (Univ.ContextSet.levels ctx) g
-  in Univ.merge_constraints (Univ.ContextSet.constraints ctx) g
+  in UGraph.merge_constraints (Univ.ContextSet.constraints ctx) g
 
 let push_context_set ?(strict=false) ctx env =
   map_universes (add_universes_set strict ctx) env
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 9f6ea522a..714c26066 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -41,7 +41,7 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool
 
 val empty_env : env
 
-val universes     : env -> Univ.universes
+val universes     : env -> UGraph.t
 val rel_context   : env -> rel_context
 val named_context : env -> named_context
 val named_context_val : env -> named_context_val
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 5a234d09b..155ad7987 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -290,7 +290,7 @@ let typecheck_inductive env mie =
       let full_polymorphic () = 
 	let defu = Term.univ_of_sort def_level in
 	let is_natural =
-	  type_in_type env || (check_leq (universes env') infu defu &&
+	  type_in_type env || (UGraph.check_leq (universes env') infu defu &&
 				not (is_type0m_univ defu && not is_unit)
 				  (* (~ is_type0m_univ defu \/ is_unit) (\* infu <= defu && not prop or unital *\) *)
 
@@ -320,7 +320,7 @@ let typecheck_inductive env mie =
 	    (* conclusions of the parameters *)
             (* We enforce [u >= lev] in case [lev] has a strict upper *)
             (* constraints over [u] *)
-	    let b = type_in_type env || check_leq (universes env') infu u in
+	    let b = type_in_type env || UGraph.check_leq (universes env') infu u in
 	      if not b then
 		anomaly ~label:"check_inductive" 
 		  (Pp.str"Incorrect universe " ++
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 29fe887d7..f7220c94a 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -1,6 +1,7 @@
 Names
 Uint31
 Univ
+UGraph
 Esubst
 Sorts
 Evar
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 922652287..0f3ea1d0a 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -104,7 +104,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
 	  let csti = Univ.enforce_eq_instances cus newus cst in
 	  let csta = Univ.Constraint.union csti ccst in
 	  let env' = Environ.push_context ~strict:false (Univ.UContext.make (inst, csta)) env in
-	  let () = if not (Univ.check_constraints cst (Environ.universes env')) then
+	  let () = if not (UGraph.check_constraints cst (Environ.universes env')) then
 		     error_incorrect_with_constraint lab
 	  in
 	  let cst = match cb.const_body with
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 5f3f559a2..615b9d49b 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -45,7 +45,7 @@ type globals = {
   env_modtypes : module_type_body MPmap.t}
 
 type stratification = {
-  env_universes : universes;
+  env_universes : UGraph.t;
   env_engagement : engagement
 }
 
@@ -93,7 +93,7 @@ let empty_env = {
   env_rel_val = [];
   env_nb_rel = 0;
   env_stratification = {
-    env_universes = initial_universes;
+    env_universes = UGraph.initial_universes;
     env_engagement = (PredicativeSet,StratifiedType) };
   env_conv_oracle = Conv_oracle.empty;
   retroknowledge = Retroknowledge.initial_retroknowledge;
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 0ce0bed23..b499ac0c5 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -32,7 +32,7 @@ type globals = {
   env_modtypes : module_type_body MPmap.t}
 
 type stratification = {
-  env_universes : universes;
+  env_universes : UGraph.t;
   env_engagement : engagement
 }
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 2cf3f8873..29c6009ce 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -147,7 +147,7 @@ let betazeta_appvect n c v =
 (* Conversion utility functions *)
 type 'a conversion_function = env -> 'a -> 'a -> unit
 type 'a trans_conversion_function = Names.transparent_state -> 'a conversion_function
-type 'a universe_conversion_function = env -> Univ.universes -> 'a -> 'a -> unit
+type 'a universe_conversion_function = env -> UGraph.t -> 'a -> 'a -> unit
 type 'a trans_universe_conversion_function = 
   Names.transparent_state -> 'a universe_conversion_function
 
@@ -180,7 +180,7 @@ type 'a universe_state = 'a * 'a universe_compare
 
 type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b
 
-type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints
+type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constraints
 
 let sort_cmp_universes env pb s0 s1 (u, check) =
   (check.compare env pb s0 s1 u, check)
@@ -560,10 +560,10 @@ let clos_fconv trans cv_pb l2r evars env univs t1 t2 =
 
 
 let check_eq univs u u' = 
-  if not (check_eq univs u u') then raise NotConvertible
+  if not (UGraph.check_eq univs u u') then raise NotConvertible
 
 let check_leq univs u u' = 
-  if not (check_leq univs u u') then raise NotConvertible
+  if not (UGraph.check_leq univs u u') then raise NotConvertible
 
 let check_sort_cmp_universes env pb s0 s1 univs =
   match (s0,s1) with
@@ -590,7 +590,7 @@ let checked_sort_cmp_universes env pb s0 s1 univs =
   check_sort_cmp_universes env pb s0 s1 univs; univs
 
 let check_convert_instances _flex u u' univs =
-  if Univ.Instance.check_eq univs u u' then univs
+  if UGraph.check_eq_instances univs u u' then univs
   else raise NotConvertible
 
 let checked_universes =
@@ -598,12 +598,12 @@ let checked_universes =
     compare_instances = check_convert_instances }
 
 let infer_eq (univs, cstrs as cuniv) u u' =
-  if Univ.check_eq univs u u' then cuniv
+  if UGraph.check_eq univs u u' then cuniv
   else
     univs, (Univ.enforce_eq u u' cstrs)
 
 let infer_leq (univs, cstrs as cuniv) u u' =
-  if Univ.check_leq univs u u' then cuniv
+  if UGraph.check_leq univs u u' then cuniv
   else
     let cstrs' = Univ.enforce_leq u u' cstrs in
       univs, cstrs'
@@ -632,7 +632,7 @@ let infer_cmp_universes env pb s0 s1 univs =
 let infer_convert_instances flex u u' (univs,cstrs) =
   (univs, Univ.enforce_eq_instances u u' cstrs)
 
-let infered_universes : (Univ.universes * Univ.Constraint.t) universe_compare = 
+let infered_universes : (UGraph.t * Univ.Constraint.t) universe_compare = 
   { compare = infer_cmp_universes;
     compare_instances = infer_convert_instances }
 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 6ced5c498..a22f3730e 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -30,7 +30,7 @@ exception NotConvertibleVect of int
 
 type 'a conversion_function = env -> 'a -> 'a -> unit
 type 'a trans_conversion_function = Names.transparent_state -> 'a conversion_function
-type 'a universe_conversion_function = env -> Univ.universes -> 'a -> 'a -> unit
+type 'a universe_conversion_function = env -> UGraph.t -> 'a -> 'a -> unit
 type 'a trans_universe_conversion_function = 
   Names.transparent_state -> 'a universe_conversion_function
 
@@ -47,10 +47,10 @@ type 'a universe_state = 'a * 'a universe_compare
 
 type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b
 
-type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints
+type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constraints
 
 val check_sort_cmp_universes :
-  env -> conv_pb -> sorts -> sorts -> Univ.universes -> unit
+  env -> conv_pb -> sorts -> sorts -> UGraph.t -> unit
 
 (* val sort_cmp : *)
 (*     conv_pb -> sorts -> sorts -> Univ.constraints -> Univ.constraints *)
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 58f3bcdf0..a00a462e1 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -317,7 +317,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 		  (* Check that the given definition does not add any constraint over
 		     the expected ones, so that it can be used in place of 
                      the original. *)
-		    if Univ.check_constraints ctx1 (Environ.universes env) then
+		    if UGraph.check_constraints ctx1 (Environ.universes env) then
 		      cstrs, env, inst2
 		    else error (IncompatibleConstraints ctx1)
 		with Univ.UniverseInconsistency incon -> 
diff --git a/kernel/term.mli b/kernel/term.mli
index 501aaf741..f8badb0dd 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -427,11 +427,11 @@ val eq_constr : constr -> constr -> bool
 
 (** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts,
    application grouping and the universe constraints in [u]. *)
-val eq_constr_univs : constr Univ.check_function
+val eq_constr_univs : constr UGraph.check_function
 
 (** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo 
     alpha, casts, application grouping and the universe constraints in [u]. *)
-val leq_constr_univs : constr Univ.check_function
+val leq_constr_univs : constr UGraph.check_function
 
 (** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts,
    application grouping and ignoring universe instances. *)
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
new file mode 100644
index 000000000..356cf4da6
--- /dev/null
+++ b/kernel/uGraph.ml
@@ -0,0 +1,868 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Errors
+open Util
+open Univ
+
+(* 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] *)
+(* Extension with algebraic universes by HH for Coq V7.0 [Sep 2001] *)
+(* Additional support for sort-polymorphic inductive types by HH [Mar 2006] *)
+(* Support for universe polymorphism by MS [2014] *)
+
+(* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey, Matthieu Sozeau, 
+   Pierre-Marie Pédrot *)
+
+let error_inconsistency o u v (p:explanation option) =
+  raise (UniverseInconsistency (o,Universe.make u,Universe.make v,p))
+
+type status = Unset | SetLe | SetLt
+
+(* Comparison on this type is pointer equality *)
+type canonical_arc =
+    { univ: Level.t;
+      lt: Level.t list;
+      le: Level.t list;
+      rank : int;
+      mutable status : status;
+      (** Guaranteed to be unset out of the [compare_neq] functions. It is used
+          to do an imperative traversal of the graph, ensuring a O(1) check that
+          a node has already been visited. Quite performance critical indeed. *)
+    }
+
+let arc_is_le arc = match arc.status with
+| Unset -> false
+| SetLe | SetLt -> true
+
+let arc_is_lt arc = match arc.status with
+| Unset | SetLe -> false
+| SetLt -> true
+
+let terminal u = {univ=u; lt=[]; le=[]; rank=0; status = Unset}
+
+module UMap :
+sig
+  type key = Level.t
+  type +'a t
+  val empty : 'a t
+  val add : key -> 'a -> 'a t -> 'a t
+  val find : key -> 'a t -> 'a
+  val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
+  val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+  val iter : (key -> 'a -> unit) -> 'a t -> unit
+  val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
+end = HMap.Make(Level)
+
+(* A Level.t is either an alias for another one, or a canonical one,
+   for which we know the universes that are above *)
+
+type univ_entry =
+    Canonical of canonical_arc
+  | Equiv of Level.t
+
+type universes = univ_entry UMap.t
+
+type t = universes
+
+(** Used to cleanup universes if a traversal function is interrupted before it
+    has the opportunity to do it itself. *)
+let unsafe_cleanup_universes g =
+  let iter _ arc = match arc with
+  | Equiv _ -> ()
+  | Canonical arc -> arc.status <- Unset
+  in
+  UMap.iter iter g
+
+let rec cleanup_universes g =
+  try unsafe_cleanup_universes g
+  with e ->
+    (** The only way unsafe_cleanup_universes 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
+
+let enter_equiv_arc u v g =
+  UMap.add u (Equiv v) g
+
+let enter_arc ca g =
+  UMap.add ca.univ (Canonical ca) g
+
+(* Every Level.t has a unique canonical arc representative *)
+
+(** The graph always contains nodes for Prop and Set. *)
+
+let terminal_lt u v =
+  {(terminal u) with lt=[v]}
+    
+let empty_universes =
+  let g = enter_arc (terminal Level.set) UMap.empty in
+  let g = enter_arc (terminal_lt Level.prop Level.set) g in
+    g
+
+(* repr : universes -> Level.t -> canonical_arc *)
+(* canonical representative : we follow the Equiv links *)
+
+let rec repr g u =
+  let a =
+    try UMap.find u g
+    with Not_found -> anomaly ~label:"Univ.repr"
+        (str"Universe " ++ Level.pr u ++ str" undefined")
+  in
+  match a with
+    | Equiv v -> repr g v
+    | Canonical arc -> arc
+
+let get_prop_arc g = repr g Level.prop
+let get_set_arc g = repr g Level.set
+let is_set_arc u = Level.is_set u.univ
+let is_prop_arc u = Level.is_prop u.univ
+
+exception AlreadyDeclared
+            
+let add_universe vlev strict g =
+  try
+    let _arcv = UMap.find vlev g in
+      raise AlreadyDeclared
+  with Not_found -> 
+    let v = terminal vlev in
+    let arc =
+      let arc = get_set_arc g in
+        if strict then
+          { arc with lt=vlev::arc.lt}
+        else 
+          { arc with le=vlev::arc.le}
+    in
+    let g = enter_arc arc g in
+      enter_arc v g
+
+(* reprleq : canonical_arc -> canonical_arc list *)
+(* All canonical arcv such that arcu<=arcv with arcv#arcu *)
+let reprleq g arcu =
+  let rec searchrec w = function
+    | [] -> w
+    | v :: vl ->
+        let arcv = repr g v in
+        if List.memq arcv w || arcu==arcv then
+          searchrec w vl
+        else
+          searchrec (arcv :: w) vl
+  in
+  searchrec [] arcu.le
+
+
+(* between : Level.t -> canonical_arc -> canonical_arc list *)
+(* between u v = { w | u<=w<=v, w canonical }          *)
+(* between is the most costly operation *)
+
+let between g arcu arcv =
+  (* good are all w | u <= w <= v  *)
+  (* bad are all w | u <= w ~<= v *)
+    (* find good and bad nodes in {w | u <= w} *)
+    (* explore b u = (b or "u is good") *)
+  let rec explore ((good, bad, b) as input) arcu =
+    if List.memq arcu good then
+      (good, bad, true) (* b or true *)
+    else if List.memq arcu bad then
+      input    (* (good, bad, b or false) *)
+    else
+      let leq = reprleq g arcu in
+        (* is some universe >= u good ? *)
+      let good, bad, b_leq =
+        List.fold_left explore (good, bad, false) leq
+      in
+        if b_leq then
+          arcu::good, bad, true (* b or true *)
+        else
+          good, arcu::bad, b    (* b or false *)
+  in
+  let good,_,_ = explore ([arcv],[],false) arcu in
+    good
+(* We assume  compare(u,v) = LE with v canonical (see compare below).
+   In this case List.hd(between g u v) = repr u
+   Otherwise, between g u v = []
+ *)
+
+(** [fast_compare_neq] : is [arcv] in the transitive upward closure of [arcu] ?
+
+  In [strict] mode, we fully distinguish between LE and LT, while in
+  non-strict mode, we simply answer LE for both situations.
+
+  If [arcv] is encountered in a LT part, we could directly answer
+  without visiting unneeded parts of this transitive closure.
+  In [strict] mode, if [arcv] is encountered in a LE part, we could only
+  change the default answer (1st arg [c]) from NLE to LE, since a strict
+  constraint may appear later. During the recursive traversal,
+  [lt_done] and [le_done] are universes we have already visited,
+  they do not contain [arcv]. The 4rd arg is [(lt_todo,le_todo)],
+  two lists of universes not yet considered, known to be above [arcu],
+  strictly or not.
+
+  We use depth-first search, but the presence of [arcv] in [new_lt]
+  is checked as soon as possible : this seems to be slightly faster
+  on a test.
+
+  We do the traversal imperatively, setting the [status] flag on visited nodes.
+  This ensures O(1) check, but it also requires unsetting the flag when leaving
+  the function. Some special care has to be taken in order to ensure we do not
+  recover a messed up graph at the end. This occurs in particular when the
+  traversal raises an exception. Even though the code below is exception-free,
+  OCaml may still raise random exceptions, essentially fatal exceptions or
+  signal handlers. Therefore we ensure the cleanup by a catch-all clause. Note
+  also that the use of an imperative solution does make this function
+  thread-unsafe. For now we do not check universes in different threads, but if
+  ever this is to be done, we would need some lock somewhere.
+
+*)
+
+let get_explanation strict g arcu arcv =
+  (* [c] characterizes whether (and how) arcv has already been related
+     to arcu among the lt_done,le_done universe *)
+  let rec cmp c to_revert lt_todo le_todo = match lt_todo, le_todo with
+  | [],[] -> (to_revert, c)
+  | (arc,p)::lt_todo, le_todo ->
+    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
+          let p = (Lt, Universe.make u) :: p in
+          if arc == arcv then
+            if strict then (to_revert, p) else (to_revert, p)
+          else find ((arc, p) :: lt_todo) lt le
+        end
+      | u :: le ->
+        let arc = repr g u in
+        let p = (Le, Universe.make u) :: p in
+        if arc == arcv then
+          if strict then (to_revert, p) else (to_revert, p)
+        else find ((arc, p) :: lt_todo) lt le
+      in
+      find lt_todo arc.lt arc.le
+  | [], (arc,p)::le_todo ->
+    if arc == arcv then
+      (* No need to continue inspecting universes above arc:
+         if arcv is strictly above arc, then we would have a cycle.
+         But we cannot answer LE yet, a stronger constraint may
+         come later from [le_todo]. *)
+      if strict then cmp p to_revert [] le_todo else (to_revert, p)
+    else
+      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 p = (Le, Universe.make u) :: p in
+            let node = (repr g u, p) 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
+          let p = (Lt, Universe.make u) :: p in
+          if arc == arcv then
+            if strict then (to_revert, p) else (to_revert, p)
+          else find ((arc, p) :: lt_todo) lt
+        in
+        find [] arc.lt
+  in
+  let start = (* if is_prop_arc arcu then [Le, make arcv.univ] else *) [] in
+  try
+    let (to_revert, c) = cmp start [] [] [(arcu, [])] in
+    (** Reset all the touched arcs. *)
+    let () = List.iter (fun arc -> arc.status <- Unset) to_revert in
+    List.rev c
+  with e ->
+    (** Unlikely event: fatal error or signal *)
+    let () = cleanup_universes g in
+    raise e
+
+let get_explanation strict g arcu arcv =
+  if !Flags.univ_print then Some (get_explanation strict g arcu arcv)
+  else None
+
+type fast_order = FastEQ | FastLT | FastLE | FastNLE
+
+let fast_compare_neq strict g arcu arcv =
+  (* [c] characterizes whether arcv has already been related
+     to arcu among the lt_done,le_done universe *)
+  let rec cmp c to_revert lt_todo le_todo = match lt_todo, le_todo with
+  | [],[] -> (to_revert, c)
+  | arc::lt_todo, le_todo ->
+    if arc_is_lt arc then
+      cmp c to_revert lt_todo le_todo
+    else
+      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:
+         if arcv is strictly above arc, then we would have a cycle.
+         But we cannot answer LE yet, a stronger constraint may
+         come later from [le_todo]. *)
+      if strict then cmp FastLE to_revert [] le_todo else (to_revert, FastLE)
+    else
+      if arc_is_le arc then
+        cmp c to_revert [] le_todo
+      else
+        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 lt le = match le with
+  | [] ->
+    begin match lt with
+    | [] -> 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 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 lt le
+
+  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 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 lt le
+
+  in
+  try
+    let (to_revert, c) = cmp FastNLE [] [] [arcu] in
+    (** Reset all the touched arcs. *)
+    let () = List.iter (fun arc -> arc.status <- Unset) to_revert in
+    c
+  with e ->
+    (** Unlikely event: fatal error or signal *)
+    let () = cleanup_universes g in
+    raise e
+
+let get_explanation_strict g arcu arcv = get_explanation true g arcu arcv
+
+let fast_compare g arcu arcv =
+  if arcu == arcv then FastEQ else fast_compare_neq true g arcu arcv
+
+let is_leq g arcu arcv =
+  arcu == arcv ||
+    (match fast_compare_neq false g arcu arcv with
+    | FastNLE -> false
+    | (FastEQ|FastLE|FastLT) -> true)
+    
+let is_lt g arcu arcv =
+  if arcu == arcv then false
+  else
+    match fast_compare_neq true g arcu arcv with
+    | FastLT -> true
+    | (FastEQ|FastLE|FastNLE) -> false
+
+(* Invariants : compare(u,v) = EQ <=> compare(v,u) = EQ
+                compare(u,v) = LT or LE => compare(v,u) = NLE
+                compare(u,v) = NLE => compare(v,u) = NLE or LE or LT
+
+   Adding u>=v is consistent iff compare(v,u) # LT
+    and then it is redundant iff compare(u,v) # NLE
+   Adding u>v is consistent iff compare(v,u) = NLE
+    and then it is redundant iff compare(u,v) = LT *)
+
+(** * Universe checks [check_eq] and [check_leq], used in coqchk *)
+
+(** First, checks on universe levels *)
+
+let check_equal g u v =
+  let arcu = repr g u and arcv = repr g v in
+    arcu == arcv
+
+let check_eq_level g u v = u == v || check_equal g u v
+
+let check_smaller g strict u v =
+  let arcu = repr g u and arcv = repr g v in
+  if strict then
+    is_lt g arcu arcv
+  else
+    is_prop_arc arcu 
+    || (is_set_arc arcu && not (is_prop_arc arcv))
+    || is_leq g arcu arcv
+
+(** Then, checks on universes *)
+
+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
+    | 0 -> check_smaller g false u v
+    | 1 -> check_smaller g true u v
+    | x when x < 0 -> check_smaller g false u v
+    | _ -> false
+
+let exists_bigger g ul l =
+  Universe.exists (fun ul' -> 
+    check_smaller_expr g ul ul') l
+
+let real_check_leq g u v =
+  Universe.for_all (fun ul -> exists_bigger g ul v) u
+    
+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
+
+(** Enforcing new constraints : [setlt], [setleq], [merge], [merge_disc] *)
+
+(* setlt : Level.t -> Level.t -> reason -> unit *)
+(* forces u > v *)
+(* this is normally an update of u in g rather than a creation. *)
+let setlt g arcu arcv =
+  let arcu' = {arcu with lt=arcv.univ::arcu.lt} in
+    enter_arc arcu' g, arcu'
+
+(* checks that non-redundant *)
+let setlt_if (g,arcu) v =
+  let arcv = repr g v in
+  if is_lt g arcu arcv then g, arcu
+  else setlt g arcu arcv
+
+(* setleq : Level.t -> Level.t -> unit *)
+(* forces u >= v *)
+(* this is normally an update of u in g rather than a creation. *)
+let setleq g arcu arcv =
+  let arcu' = {arcu with le=arcv.univ::arcu.le} in
+    enter_arc arcu' g, arcu'
+
+(* checks that non-redundant *)
+let setleq_if (g,arcu) v =
+  let arcv = repr g v in
+  if is_leq g arcu arcv then g, arcu
+  else setleq g arcu arcv
+
+(* merge : Level.t -> Level.t -> unit *)
+(* we assume  compare(u,v) = LE *)
+(* merge u v  forces u ~ v with repr u as canonical repr *)
+let merge g arcu arcv =
+  (* we find the arc with the biggest rank, and we redirect all others to it *)
+  let arcu, g, v =
+    let best_ranked (max_rank, old_max_rank, best_arc, rest) arc =
+      if Level.is_small arc.univ ||
+           (arc.rank >= max_rank && not (Level.is_small best_arc.univ))
+      then (arc.rank, max_rank, arc, best_arc::rest)
+      else (max_rank, old_max_rank, best_arc, arc::rest)
+    in
+      match between g arcu arcv with
+      | [] -> anomaly (str "Univ.between")
+      | arc::rest ->
+        let (max_rank, old_max_rank, best_arc, rest) =
+          List.fold_left best_ranked (arc.rank, min_int, arc, []) rest in
+          if max_rank > old_max_rank then best_arc, g, rest
+          else begin
+              (* one redirected node also has max_rank *)
+            let arcu = {best_arc with rank = max_rank + 1} in
+              arcu, enter_arc arcu g, rest
+          end 
+  in
+  let redirect (g,w,w') arcv =
+    let g' = enter_equiv_arc arcv.univ arcu.univ g in
+    (g',List.unionq arcv.lt w,arcv.le@w')
+  in
+  let (g',w,w') = List.fold_left redirect (g,[],[]) v in
+  let g_arcu = (g',arcu) in
+  let g_arcu = List.fold_left setlt_if g_arcu w in
+  let g_arcu = List.fold_left setleq_if g_arcu w' in
+  fst g_arcu
+
+(* merge_disc : Level.t -> Level.t -> unit *)
+(* we assume  compare(u,v) = compare(v,u) = NLE *)
+(* merge_disc u v  forces u ~ v with repr u as canonical repr *)
+let merge_disc g arc1 arc2 =
+  let arcu, arcv = if Level.is_small arc2.univ || arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in
+  let arcu, g = 
+    if not (Int.equal arc1.rank arc2.rank) then arcu, g
+    else
+      let arcu = {arcu with rank = succ arcu.rank} in 
+      arcu, enter_arc arcu g
+  in
+  let g' = enter_equiv_arc arcv.univ arcu.univ g in
+  let g_arcu = (g',arcu) in
+  let g_arcu = List.fold_left setlt_if g_arcu arcv.lt in
+  let g_arcu = List.fold_left setleq_if g_arcu arcv.le in
+  fst g_arcu
+
+(* enforce_univ_eq : Level.t -> Level.t -> unit *)
+(* enforce_univ_eq u v will force u=v if possible, will fail otherwise *)
+
+let enforce_univ_eq u v g =
+  let arcu = repr g u and arcv = repr g v in
+    match fast_compare g arcu arcv with
+    | FastEQ -> g
+    | FastLT ->
+      let p = get_explanation_strict g arcu arcv in
+      error_inconsistency Eq v u p
+    | FastLE -> merge g arcu arcv
+    | FastNLE ->
+      (match fast_compare g arcv arcu with
+      | FastLT ->
+        let p = get_explanation_strict g arcv arcu in
+        error_inconsistency Eq u v p
+      | FastLE -> merge g arcv arcu
+      | FastNLE -> merge_disc g arcu arcv
+      | FastEQ -> anomaly (Pp.str "Univ.compare"))
+
+(* enforce_univ_leq : Level.t -> Level.t -> unit *)
+(* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *)
+let enforce_univ_leq u v g =
+  let arcu = repr g u and arcv = repr g v in
+  if is_leq g arcu arcv then g
+  else
+    match fast_compare g arcv arcu with
+    | FastLT ->
+      let p = get_explanation_strict g arcv arcu in
+      error_inconsistency Le u v p
+    | FastLE  -> merge g arcv arcu
+    | FastNLE -> fst (setleq g arcu arcv)
+    | FastEQ -> anomaly (Pp.str "Univ.compare")
+
+(* enforce_univ_lt u v will force u<v if possible, will fail otherwise *)
+let enforce_univ_lt u v g =
+  let arcu = repr g u and arcv = repr g v in
+    match fast_compare g arcu arcv with
+    | FastLT -> g
+    | FastLE -> fst (setlt g arcu arcv)
+    | FastEQ -> error_inconsistency Lt u v (Some [(Eq,Universe.make v)])
+    | FastNLE ->
+      match fast_compare_neq false g arcv arcu with
+        FastNLE -> fst (setlt g arcu arcv)
+      | FastEQ -> anomaly (Pp.str "Univ.compare")
+      | (FastLE|FastLT) ->
+        let p = get_explanation false g arcv arcu  in
+        error_inconsistency Lt u v p
+
+(* Prop = Set is forbidden here. *)
+let initial_universes = empty_universes
+
+let is_initial_universes g = UMap.equal (==) g initial_universes
+      
+let enforce_constraint cst g =
+  match cst with
+    | (u,Lt,v) -> enforce_univ_lt u v g
+    | (u,Le,v) -> enforce_univ_leq u v g
+    | (u,Eq,v) -> enforce_univ_eq u v g
+      
+let merge_constraints c g =
+  Constraint.fold enforce_constraint c g
+
+let check_constraint g (l,d,r) =
+  match d with
+  | Eq -> check_equal g l r
+  | Le -> check_smaller g false l r
+  | Lt -> check_smaller g true l r
+
+let check_constraints c g =
+  Constraint.for_all (check_constraint g) c
+
+(* Normalization *)
+
+let lookup_level u g =
+  try Some (UMap.find u g) with Not_found -> None
+
+(** [normalize_universes 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
+    (see the assertion)... I (Stéphane Glondu) am not sure if this
+    plays a role in the rest of the module. *)
+let normalize_universes g =
+  let rec visit u arc cache = match lookup_level u cache with
+    | Some x -> x, cache
+    | None -> match Lazy.force arc with
+    | None ->
+      u, UMap.add u u cache
+    | Some (Canonical {univ=v; lt=_; le=_}) ->
+      v, UMap.add u v cache
+    | Some (Equiv v) ->
+      let v, cache = visit v (lazy (lookup_level v g)) cache in
+      v, UMap.add u v cache
+  in
+  let cache = UMap.fold
+    (fun u arc cache -> snd (visit u (Lazy.lazy_from_val (Some arc)) cache))
+    g UMap.empty
+  in
+  let repr x = UMap.find x cache in
+  let lrepr us = List.fold_left
+    (fun e x -> LSet.add (repr x) e) LSet.empty us
+  in
+  let canonicalize u = function
+    | Equiv _ -> Equiv (repr u)
+    | Canonical {univ=v; lt=lt; le=le; rank=rank} ->
+      assert (u == v);
+      (* avoid duplicates and self-loops *)
+      let lt = lrepr lt and le = lrepr le in
+      let le = LSet.filter
+        (fun x -> x != u && not (LSet.mem x lt)) le
+      in
+      LSet.iter (fun x -> assert (x != u)) lt;
+      Canonical {
+        univ = v;
+        lt = LSet.elements lt;
+        le = LSet.elements le;
+        rank = rank;
+        status = Unset;
+      }
+  in
+  UMap.mapi canonicalize g
+
+let constraints_of_universes g =
+  let constraints_of u v acc =
+    match v with
+    | Canonical {univ=u; lt=lt; le=le} ->
+      let acc = List.fold_left (fun acc v -> Constraint.add (u,Lt,v) acc) acc lt in
+      let acc = List.fold_left (fun acc v -> Constraint.add (u,Le,v) acc) acc le in
+        acc
+    | Equiv v -> Constraint.add (u,Eq,v) acc
+  in
+  UMap.fold constraints_of g Constraint.empty
+
+let constraints_of_universes g =
+  constraints_of_universes (normalize_universes g)
+
+(** Longest path algorithm. This is used to compute the minimal number of
+    universes required if the only strict edge would be the Lt one. This
+    algorithm assumes that the given universes constraints are a almost DAG, in
+    the sense that there may be {Eq, Le}-cycles. This is OK for consistent
+    universes, which is the only case where we use this algorithm. *)
+
+(** Adjacency graph *)
+type graph = constraint_type LMap.t LMap.t
+
+exception Connected
+
+(** Check connectedness *)
+let connected x y (g : graph) =
+  let rec connected x target seen g =
+    if Level.equal x target then raise Connected
+    else if not (LSet.mem x seen) then
+      let seen = LSet.add x seen in
+      let fold z _ seen = connected z target seen g in
+      let neighbours = try LMap.find x g with Not_found -> LMap.empty in
+      LMap.fold fold neighbours seen
+    else seen
+  in
+  try ignore(connected x y LSet.empty g); false with Connected -> true
+
+let add_edge x y v (g : graph) =
+  try
+    let neighbours = LMap.find x g in
+    let neighbours = LMap.add y v neighbours in
+    LMap.add x neighbours g
+  with Not_found ->
+    LMap.add x (LMap.singleton y v) g
+
+(** We want to keep the graph DAG. If adding an edge would cause a cycle, that
+    would necessarily be an {Eq, Le}-cycle, otherwise there would have been a
+    universe inconsistency. Therefore we may omit adding such a cycling edge
+    without changing the compacted graph. *)
+let add_eq_edge x y v g = if connected y x g then g else add_edge x y v g
+
+(** Construct the DAG and its inverse at the same time. *)
+let make_graph g : (graph * graph) =
+  let fold u arc accu = match arc with
+  | Equiv v ->
+    let (dir, rev) = accu in
+    (add_eq_edge u v Eq dir, add_eq_edge v u Eq rev)
+  | Canonical { univ; lt; le; } ->
+    let () = assert (u == univ) in
+    let fold_lt (dir, rev) v = (add_edge u v Lt dir, add_edge v u Lt rev) in
+    let fold_le (dir, rev) v = (add_eq_edge u v Le dir, add_eq_edge v u Le rev) in
+    (** Order is important : lt after le, because of the possible redundancy
+        between [le] and [lt] in a canonical arc. This way, the [lt] constraint
+        is the last one set, which is correct because it implies [le]. *)
+    let accu = List.fold_left fold_le accu le in
+    let accu = List.fold_left fold_lt accu lt in
+    accu
+  in
+  UMap.fold fold g (LMap.empty, LMap.empty)
+
+(** Construct a topological order out of a DAG. *)
+let rec topological_fold u g rem seen accu =
+  let is_seen =
+    try
+      let status = LMap.find u seen in
+      assert status; (** If false, not a DAG! *)
+      true
+    with Not_found -> false
+  in
+  if not is_seen then
+    let rem = LMap.remove u rem in
+    let seen = LMap.add u false seen in
+    let neighbours = try LMap.find u g with Not_found -> LMap.empty in
+    let fold v _ (rem, seen, accu) = topological_fold v g rem seen accu in
+    let (rem, seen, accu) = LMap.fold fold neighbours (rem, seen, accu) in
+    (rem, LMap.add u true seen, u :: accu)
+  else (rem, seen, accu)
+
+let rec topological g rem seen accu =
+  let node = try Some (LMap.choose rem) with Not_found -> None in
+  match node with
+  | None -> accu
+  | Some (u, _) ->
+    let rem, seen, accu = topological_fold u g rem seen accu in
+    topological g rem seen accu
+
+(** Compute the longest path from any vertex. *)
+let constraint_cost = function
+| Eq | Le -> 0
+| Lt -> 1
+
+(** This algorithm browses the graph in topological order, computing for each
+    encountered node the length of the longest path leading to it. Should be
+    O(|V|) or so (modulo map representation). *)
+let rec flatten_graph rem (rev : graph) map mx = match rem with
+| [] -> map, mx
+| u :: rem ->
+  let prev = try LMap.find u rev with Not_found -> LMap.empty in
+  let fold v cstr accu =
+    let v_cost = LMap.find v map in
+    max (v_cost + constraint_cost cstr) accu
+  in
+  let u_cost = LMap.fold fold prev 0 in
+  let map = LMap.add u u_cost map in
+  flatten_graph rem rev map (max mx u_cost)
+
+(** [sort_universes g] builds a map from universes in [g] to natural
+    numbers. It outputs a graph containing equivalence edges from each
+    level appearing in [g] to [Type.n], and [lt] edges between the
+    [Type.n]s. The output graph should imply the input graph (and the
+    [Type.n]s. The output graph should imply the input graph (and the
+    implication will be strict most of the time), but is not
+    necessarily minimal. 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_universes orig =
+  let (dir, rev) = make_graph orig in
+  let order = topological dir dir LMap.empty [] in
+  let compact, max = flatten_graph order rev LMap.empty 0 in
+  let mp = Names.DirPath.make [Names.Id.of_string "Type"] in
+  let types = Array.init (max + 1) (fun n -> Level.make mp n) in
+  (** Old universes are made equal to [Type.n] *)
+  let fold u level accu = UMap.add u (Equiv types.(level)) accu in
+  let sorted = LMap.fold fold compact UMap.empty in
+  (** Add all [Type.n] nodes *)
+  let fold i accu u =
+    if i < max then
+      let pred = types.(i + 1) in
+      let arc = {univ = u; lt = [pred]; le = []; rank = 0; status = Unset; } in
+      UMap.add u (Canonical arc) accu
+    else accu
+  in
+  Array.fold_left_i fold sorted types
+
+(** Instances *)
+
+let check_eq_instances g t1 t2 =
+  let t1 = Instance.to_array t1 in
+  let t2 = Instance.to_array t2 in
+  t1 == t2 ||
+    (Int.equal (Array.length t1) (Array.length t2) &&
+        let rec aux i =
+          (Int.equal i (Array.length t1)) || (check_eq_level g t1.(i) t2.(i) && aux (i + 1))
+        in aux 0)
+
+let pr_arc prl = function
+  | _, Canonical {univ=u; lt=[]; le=[]} ->
+      mt ()
+  | _, Canonical {univ=u; lt=lt; le=le} ->
+      let opt_sep = match lt, le with
+      | [], _ | _, [] -> mt ()
+      | _ -> spc ()
+      in
+      prl u ++ str " " ++
+      v 0
+        (pr_sequence (fun v -> str "< " ++ prl v) lt ++
+         opt_sep ++
+         pr_sequence (fun v -> str "<= " ++ prl v) le) ++
+      fnl ()
+  | u, Equiv v ->
+      prl u  ++ str " = " ++ prl v ++ fnl ()
+
+let pr_universes prl g =
+  let graph = UMap.fold (fun u a l -> (u,a)::l) g [] in
+  prlist (pr_arc prl) graph
+
+(* Dumping constraints to a file *)
+
+let dump_universes output g =
+  let dump_arc u = function
+    | Canonical {univ=u; lt=lt; le=le} ->
+        let u_str = Level.to_string u in
+        List.iter (fun v -> output Lt (Level.to_string v) u_str) lt;
+        List.iter (fun v -> output Le (Level.to_string v) u_str) le
+    | Equiv v ->
+      output Eq (Level.to_string u) (Level.to_string v)
+  in
+  UMap.iter dump_arc g
+
+(** Profiling *)
+
+let merge_constraints = 
+  if Flags.profile then 
+    let key = Profile.declare_profile "merge_constraints" in
+      Profile.profile2 key merge_constraints
+  else merge_constraints
+
+let check_constraints =
+  if Flags.profile then
+    let key = Profile.declare_profile "check_constraints" in
+      Profile.profile2 key check_constraints
+  else check_constraints
+
+let check_eq = 
+  if Flags.profile then
+    let check_eq_key = Profile.declare_profile "check_eq" in
+      Profile.profile3 check_eq_key check_eq
+  else check_eq
+
+let check_leq = 
+  if Flags.profile then 
+    let check_leq_key = Profile.declare_profile "check_leq" in
+      Profile.profile3 check_leq_key check_leq
+  else check_leq
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
new file mode 100644
index 000000000..e95cf4d1c
--- /dev/null
+++ b/kernel/uGraph.mli
@@ -0,0 +1,63 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Univ
+
+(** {6 Graphs of universes. } *)
+
+type t
+
+type universes = t
+
+type 'a check_function = universes -> 'a -> 'a -> bool
+val check_leq : universe check_function
+val check_eq : universe check_function
+
+(** The empty graph of universes *)
+val empty_universes : universes
+
+(** The initial graph of universes: Prop < Set *)
+val initial_universes : universes
+
+val is_initial_universes : universes -> bool
+
+val sort_universes : universes -> universes
+
+(** Adds a universe to the graph, ensuring it is >= or > Set.
+   @raises AlreadyDeclared if the level is already declared in the graph. *)
+
+exception AlreadyDeclared
+
+val add_universe : universe_level -> bool -> universes -> universes
+
+(** {6 ... } *)
+(** Merge of constraints in a universes graph.
+  The function [merge_constraints] merges a set of constraints in a given
+  universes graph. It raises the exception [UniverseInconsistency] if the
+  constraints are not satisfiable. *)
+
+val enforce_constraint : univ_constraint -> universes -> universes
+val merge_constraints : constraints -> universes -> universes
+
+val constraints_of_universes : universes -> constraints
+
+val check_constraint  : universes -> univ_constraint -> bool
+val check_constraints : constraints -> universes -> bool
+
+val check_eq_instances : Instance.t check_function
+(** Check equality of instances w.r.t. a universe graph *)
+
+(** {6 Pretty-printing of universes. } *)
+
+val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds
+
+(** {6 Dumping to a file } *)
+
+val dump_universes :
+  (constraint_type -> string -> string -> unit) ->
+  universes -> unit
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 34eb283d7..7e6d4de23 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -653,170 +653,6 @@ open Universe
 
 let universe_level = Universe.level
 
-type status = Unset | SetLe | SetLt
-
-(* Comparison on this type is pointer equality *)
-type canonical_arc =
-    { univ: Level.t;
-      lt: Level.t list;
-      le: Level.t list;
-      rank : int;
-      mutable status : status;
-      (** Guaranteed to be unset out of the [compare_neq] functions. It is used
-          to do an imperative traversal of the graph, ensuring a O(1) check that
-          a node has already been visited. Quite performance critical indeed. *)
-    }
-
-let arc_is_le arc = match arc.status with
-| Unset -> false
-| SetLe | SetLt -> true
-
-let arc_is_lt arc = match arc.status with
-| Unset | SetLe -> false
-| SetLt -> true
-
-let terminal u = {univ=u; lt=[]; le=[]; rank=0; status = Unset}
-
-module UMap :
-sig
-  type key = Level.t
-  type +'a t
-  val empty : 'a t
-  val add : key -> 'a -> 'a t -> 'a t
-  val find : key -> 'a t -> 'a
-  val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
-  val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
-  val iter : (key -> 'a -> unit) -> 'a t -> unit
-  val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
-end = HMap.Make(Level)
-
-(* A Level.t is either an alias for another one, or a canonical one,
-   for which we know the universes that are above *)
-
-type univ_entry =
-    Canonical of canonical_arc
-  | Equiv of Level.t
-
-type universes = univ_entry UMap.t
-
-(** Used to cleanup universes if a traversal function is interrupted before it
-    has the opportunity to do it itself. *)
-let unsafe_cleanup_universes g =
-  let iter _ arc = match arc with
-  | Equiv _ -> ()
-  | Canonical arc -> arc.status <- Unset
-  in
-  UMap.iter iter g
-
-let rec cleanup_universes g =
-  try unsafe_cleanup_universes g
-  with e ->
-    (** The only way unsafe_cleanup_universes 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
-
-let enter_equiv_arc u v g =
-  UMap.add u (Equiv v) g
-
-let enter_arc ca g =
-  UMap.add ca.univ (Canonical ca) g
-
-(* Every Level.t has a unique canonical arc representative *)
-
-(** The graph always contains nodes for Prop and Set. *)
-
-let terminal_lt u v =
-  {(terminal u) with lt=[v]}
-    
-let empty_universes =
-  let g = enter_arc (terminal Level.set) UMap.empty in
-  let g = enter_arc (terminal_lt Level.prop Level.set) g in
-    g
-
-(* repr : universes -> Level.t -> canonical_arc *)
-(* canonical representative : we follow the Equiv links *)
-
-let rec repr g u =
-  let a =
-    try UMap.find u g
-    with Not_found -> anomaly ~label:"Univ.repr"
-        (str"Universe " ++ Level.pr u ++ str" undefined")
-  in
-  match a with
-    | Equiv v -> repr g v
-    | Canonical arc -> arc
-
-let get_prop_arc g = repr g Level.prop
-let get_set_arc g = repr g Level.set
-let is_set_arc u = Level.is_set u.univ
-let is_prop_arc u = Level.is_prop u.univ
-
-exception AlreadyDeclared
-	    
-let add_universe vlev strict g =
-  try
-    let _arcv = UMap.find vlev g in
-      raise AlreadyDeclared
-  with Not_found -> 
-    let v = terminal vlev in
-    let arc =
-      let arc = get_set_arc g in
-	if strict then
-	  { arc with lt=vlev::arc.lt}
-	else 
-	  { arc with le=vlev::arc.le}
-    in
-    let g = enter_arc arc g in
-      enter_arc v g
-
-(* reprleq : canonical_arc -> canonical_arc list *)
-(* All canonical arcv such that arcu<=arcv with arcv#arcu *)
-let reprleq g arcu =
-  let rec searchrec w = function
-    | [] -> w
-    | v :: vl ->
-	let arcv = repr g v in
-        if List.memq arcv w || arcu==arcv then
-	  searchrec w vl
-        else
-	  searchrec (arcv :: w) vl
-  in
-  searchrec [] arcu.le
-
-
-(* between : Level.t -> canonical_arc -> canonical_arc list *)
-(* between u v = { w | u<=w<=v, w canonical }          *)
-(* between is the most costly operation *)
-
-let between g arcu arcv =
-  (* good are all w | u <= w <= v  *)
-  (* bad are all w | u <= w ~<= v *)
-    (* find good and bad nodes in {w | u <= w} *)
-    (* explore b u = (b or "u is good") *)
-  let rec explore ((good, bad, b) as input) arcu =
-    if List.memq arcu good then
-      (good, bad, true) (* b or true *)
-    else if List.memq arcu bad then
-      input    (* (good, bad, b or false) *)
-    else
-      let leq = reprleq g arcu in
-	(* is some universe >= u good ? *)
-      let good, bad, b_leq =
-	List.fold_left explore (good, bad, false) leq
-      in
-	if b_leq then
-	  arcu::good, bad, true (* b or true *)
-	else
-	  good, arcu::bad, b    (* b or false *)
-  in
-  let good,_,_ = explore ([arcv],[],false) arcu in
-    good
-(* We assume  compare(u,v) = LE with v canonical (see compare below).
-   In this case List.hd(between g u v) = repr u
-   Otherwise, between g u v = []
- *)
 
 type constraint_type = Lt | Le | Eq
 
@@ -831,343 +667,6 @@ let constraint_type_ord c1 c2 = match c1, c2 with
 | Eq, Eq -> 0
 | Eq, _ -> 1
 
-(** [fast_compare_neq] : is [arcv] in the transitive upward closure of [arcu] ?
-
-  In [strict] mode, we fully distinguish between LE and LT, while in
-  non-strict mode, we simply answer LE for both situations.
-
-  If [arcv] is encountered in a LT part, we could directly answer
-  without visiting unneeded parts of this transitive closure.
-  In [strict] mode, if [arcv] is encountered in a LE part, we could only
-  change the default answer (1st arg [c]) from NLE to LE, since a strict
-  constraint may appear later. During the recursive traversal,
-  [lt_done] and [le_done] are universes we have already visited,
-  they do not contain [arcv]. The 4rd arg is [(lt_todo,le_todo)],
-  two lists of universes not yet considered, known to be above [arcu],
-  strictly or not.
-
-  We use depth-first search, but the presence of [arcv] in [new_lt]
-  is checked as soon as possible : this seems to be slightly faster
-  on a test.
-
-  We do the traversal imperatively, setting the [status] flag on visited nodes.
-  This ensures O(1) check, but it also requires unsetting the flag when leaving
-  the function. Some special care has to be taken in order to ensure we do not
-  recover a messed up graph at the end. This occurs in particular when the
-  traversal raises an exception. Even though the code below is exception-free,
-  OCaml may still raise random exceptions, essentially fatal exceptions or
-  signal handlers. Therefore we ensure the cleanup by a catch-all clause. Note
-  also that the use of an imperative solution does make this function
-  thread-unsafe. For now we do not check universes in different threads, but if
-  ever this is to be done, we would need some lock somewhere.
-
-*)
-
-let get_explanation strict g arcu arcv =
-  (* [c] characterizes whether (and how) arcv has already been related
-     to arcu among the lt_done,le_done universe *)
-  let rec cmp c to_revert lt_todo le_todo = match lt_todo, le_todo with
-  | [],[] -> (to_revert, c)
-  | (arc,p)::lt_todo, le_todo ->
-    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
-          let p = (Lt, make u) :: p in
-          if arc == arcv then
-            if strict then (to_revert, p) else (to_revert, p)
-          else find ((arc, p) :: lt_todo) lt le
-        end
-      | u :: le ->
-        let arc = repr g u in
-        let p = (Le, make u) :: p in
-        if arc == arcv then
-          if strict then (to_revert, p) else (to_revert, p)
-        else find ((arc, p) :: lt_todo) lt le
-      in
-      find lt_todo arc.lt arc.le
-  | [], (arc,p)::le_todo ->
-    if arc == arcv then
-      (* No need to continue inspecting universes above arc:
-	 if arcv is strictly above arc, then we would have a cycle.
-         But we cannot answer LE yet, a stronger constraint may
-	 come later from [le_todo]. *)
-      if strict then cmp p to_revert [] le_todo else (to_revert, p)
-    else
-      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 p = (Le, make u) :: p in
-            let node = (repr g u, p) 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
-          let p = (Lt, make u) :: p in
-          if arc == arcv then
-            if strict then (to_revert, p) else (to_revert, p)
-          else find ((arc, p) :: lt_todo) lt
-        in
-        find [] arc.lt
-  in
-  let start = (* if is_prop_arc arcu then [Le, make arcv.univ] else *) [] in
-  try
-    let (to_revert, c) = cmp start [] [] [(arcu, [])] in
-    (** Reset all the touched arcs. *)
-    let () = List.iter (fun arc -> arc.status <- Unset) to_revert in
-    List.rev c
-  with e ->
-    (** Unlikely event: fatal error or signal *)
-    let () = cleanup_universes g in
-    raise e
-
-let get_explanation strict g arcu arcv =
-  if !Flags.univ_print then Some (get_explanation strict g arcu arcv)
-  else None
-
-type fast_order = FastEQ | FastLT | FastLE | FastNLE
-
-let fast_compare_neq strict g arcu arcv =
-  (* [c] characterizes whether arcv has already been related
-     to arcu among the lt_done,le_done universe *)
-  let rec cmp c to_revert lt_todo le_todo = match lt_todo, le_todo with
-  | [],[] -> (to_revert, c)
-  | arc::lt_todo, le_todo ->
-    if arc_is_lt arc then
-      cmp c to_revert lt_todo le_todo
-    else
-      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:
-	 if arcv is strictly above arc, then we would have a cycle.
-         But we cannot answer LE yet, a stronger constraint may
-	 come later from [le_todo]. *)
-      if strict then cmp FastLE to_revert [] le_todo else (to_revert, FastLE)
-    else
-      if arc_is_le arc then
-        cmp c to_revert [] le_todo
-      else
-        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 lt le = match le with
-  | [] ->
-    begin match lt with
-    | [] -> 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 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 lt le
-
-  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 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 lt le
-
-  in
-  try
-    let (to_revert, c) = cmp FastNLE [] [] [arcu] in
-    (** Reset all the touched arcs. *)
-    let () = List.iter (fun arc -> arc.status <- Unset) to_revert in
-    c
-  with e ->
-    (** Unlikely event: fatal error or signal *)
-    let () = cleanup_universes g in
-    raise e
-
-let get_explanation_strict g arcu arcv = get_explanation true g arcu arcv
-
-let fast_compare g arcu arcv =
-  if arcu == arcv then FastEQ else fast_compare_neq true g arcu arcv
-
-let is_leq g arcu arcv =
-  arcu == arcv ||
-    (match fast_compare_neq false g arcu arcv with
-    | FastNLE -> false
-    | (FastEQ|FastLE|FastLT) -> true)
-    
-let is_lt g arcu arcv =
-  if arcu == arcv then false
-  else
-    match fast_compare_neq true g arcu arcv with
-    | FastLT -> true
-    | (FastEQ|FastLE|FastNLE) -> false
-
-(* Invariants : compare(u,v) = EQ <=> compare(v,u) = EQ
-                compare(u,v) = LT or LE => compare(v,u) = NLE
-                compare(u,v) = NLE => compare(v,u) = NLE or LE or LT
-
-   Adding u>=v is consistent iff compare(v,u) # LT
-    and then it is redundant iff compare(u,v) # NLE
-   Adding u>v is consistent iff compare(v,u) = NLE
-    and then it is redundant iff compare(u,v) = LT *)
-
-(** * Universe checks [check_eq] and [check_leq], used in coqchk *)
-
-(** First, checks on universe levels *)
-
-let check_equal g u v =
-  let arcu = repr g u and arcv = repr g v in
-    arcu == arcv
-
-let check_eq_level g u v = u == v || check_equal g u v
-
-let check_smaller g strict u v =
-  let arcu = repr g u and arcv = repr g v in
-  if strict then
-    is_lt g arcu arcv
-  else
-    is_prop_arc arcu 
-    || (is_set_arc arcu && not (is_prop_arc arcv))
-    || is_leq g arcu arcv
-
-(** Then, checks on universes *)
-
-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 = Huniv.exists (fun x2 -> f x1 x2) l in
-    Huniv.for_all (fun x1 -> exists x1 l2) l1
-    && Huniv.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
-    | 0 -> check_smaller g false u v
-    | 1 -> check_smaller g true u v
-    | x when x < 0 -> check_smaller g false u v
-    | _ -> false
-
-let exists_bigger g ul l =
-  Huniv.exists (fun ul' -> 
-    check_smaller_expr g ul ul') l
-
-let real_check_leq g u v =
-  Huniv.for_all (fun ul -> exists_bigger g ul v) u
-    
-let check_leq g u v =
-  Universe.equal u v ||
-    Universe.is_type0m u ||
-    check_eq_univs g u v || real_check_leq g u v
-
-(** Enforcing new constraints : [setlt], [setleq], [merge], [merge_disc] *)
-
-(* setlt : Level.t -> Level.t -> reason -> unit *)
-(* forces u > v *)
-(* this is normally an update of u in g rather than a creation. *)
-let setlt g arcu arcv =
-  let arcu' = {arcu with lt=arcv.univ::arcu.lt} in
-    enter_arc arcu' g, arcu'
-
-(* checks that non-redundant *)
-let setlt_if (g,arcu) v =
-  let arcv = repr g v in
-  if is_lt g arcu arcv then g, arcu
-  else setlt g arcu arcv
-
-(* setleq : Level.t -> Level.t -> unit *)
-(* forces u >= v *)
-(* this is normally an update of u in g rather than a creation. *)
-let setleq g arcu arcv =
-  let arcu' = {arcu with le=arcv.univ::arcu.le} in
-    enter_arc arcu' g, arcu'
-
-(* checks that non-redundant *)
-let setleq_if (g,arcu) v =
-  let arcv = repr g v in
-  if is_leq g arcu arcv then g, arcu
-  else setleq g arcu arcv
-
-(* merge : Level.t -> Level.t -> unit *)
-(* we assume  compare(u,v) = LE *)
-(* merge u v  forces u ~ v with repr u as canonical repr *)
-let merge g arcu arcv =
-  (* we find the arc with the biggest rank, and we redirect all others to it *)
-  let arcu, g, v =
-    let best_ranked (max_rank, old_max_rank, best_arc, rest) arc =
-      if Level.is_small arc.univ ||
-	   (arc.rank >= max_rank && not (Level.is_small best_arc.univ))
-      then (arc.rank, max_rank, arc, best_arc::rest)
-      else (max_rank, old_max_rank, best_arc, arc::rest)
-    in
-      match between g arcu arcv with
-      | [] -> anomaly (str "Univ.between")
-      | arc::rest ->
-        let (max_rank, old_max_rank, best_arc, rest) =
-          List.fold_left best_ranked (arc.rank, min_int, arc, []) rest in
-          if max_rank > old_max_rank then best_arc, g, rest
-          else begin
-              (* one redirected node also has max_rank *)
-            let arcu = {best_arc with rank = max_rank + 1} in
-	      arcu, enter_arc arcu g, rest
-          end 
-  in
-  let redirect (g,w,w') arcv =
-    let g' = enter_equiv_arc arcv.univ arcu.univ g in
-    (g',List.unionq arcv.lt w,arcv.le@w')
-  in
-  let (g',w,w') = List.fold_left redirect (g,[],[]) v in
-  let g_arcu = (g',arcu) in
-  let g_arcu = List.fold_left setlt_if g_arcu w in
-  let g_arcu = List.fold_left setleq_if g_arcu w' in
-  fst g_arcu
-
-(* merge_disc : Level.t -> Level.t -> unit *)
-(* we assume  compare(u,v) = compare(v,u) = NLE *)
-(* merge_disc u v  forces u ~ v with repr u as canonical repr *)
-let merge_disc g arc1 arc2 =
-  let arcu, arcv = if Level.is_small arc2.univ || arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in
-  let arcu, g = 
-    if not (Int.equal arc1.rank arc2.rank) then arcu, g
-    else
-      let arcu = {arcu with rank = succ arcu.rank} in 
-      arcu, enter_arc arcu g
-  in
-  let g' = enter_equiv_arc arcv.univ arcu.univ g in
-  let g_arcu = (g',arcu) in
-  let g_arcu = List.fold_left setlt_if g_arcu arcv.lt in
-  let g_arcu = List.fold_left setleq_if g_arcu arcv.le in
-  fst g_arcu
-
 (* Universe inconsistency: error raised when trying to enforce a relation
    that would create a cycle in the graph of universes. *)
 
@@ -1178,70 +677,10 @@ exception UniverseInconsistency of univ_inconsistency
 let error_inconsistency o u v (p:explanation option) =
   raise (UniverseInconsistency (o,make u,make v,p))
 
-(* enforce_univ_eq : Level.t -> Level.t -> unit *)
-(* enforce_univ_eq u v will force u=v if possible, will fail otherwise *)
-
-let enforce_univ_eq u v g =
-  let arcu = repr g u and arcv = repr g v in
-    match fast_compare g arcu arcv with
-    | FastEQ -> g
-    | FastLT ->
-      let p = get_explanation_strict g arcu arcv in
-      error_inconsistency Eq v u p
-    | FastLE -> merge g arcu arcv
-    | FastNLE ->
-      (match fast_compare g arcv arcu with
-      | FastLT ->
-        let p = get_explanation_strict g arcv arcu in
-        error_inconsistency Eq u v p
-      | FastLE -> merge g arcv arcu
-      | FastNLE -> merge_disc g arcu arcv
-      | FastEQ -> anomaly (Pp.str "Univ.compare"))
-
-(* enforce_univ_leq : Level.t -> Level.t -> unit *)
-(* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *)
-let enforce_univ_leq u v g =
-  let arcu = repr g u and arcv = repr g v in
-  if is_leq g arcu arcv then g
-  else
-    match fast_compare g arcv arcu with
-    | FastLT ->
-      let p = get_explanation_strict g arcv arcu in
-      error_inconsistency Le u v p
-    | FastLE  -> merge g arcv arcu
-    | FastNLE -> fst (setleq g arcu arcv)
-    | FastEQ -> anomaly (Pp.str "Univ.compare")
-
-(* enforce_univ_lt u v will force u<v if possible, will fail otherwise *)
-let enforce_univ_lt u v g =
-  let arcu = repr g u and arcv = repr g v in
-    match fast_compare g arcu arcv with
-    | FastLT -> g
-    | FastLE -> fst (setlt g arcu arcv)
-    | FastEQ -> error_inconsistency Lt u v (Some [(Eq,make v)])
-    | FastNLE ->
-      match fast_compare_neq false g arcv arcu with
-	FastNLE -> fst (setlt g arcu arcv)
-      | FastEQ -> anomaly (Pp.str "Univ.compare")
-      | (FastLE|FastLT) ->
-        let p = get_explanation false g arcv arcu  in
-        error_inconsistency Lt u v p
-
-(* Prop = Set is forbidden here. *)
-let initial_universes = empty_universes
-
-let is_initial_universes g = UMap.equal (==) g initial_universes
-      
 (* Constraints and sets of constraints. *)    
 
 type univ_constraint = Level.t * constraint_type * Level.t
 
-let enforce_constraint cst g =
-  match cst with
-    | (u,Lt,v) -> enforce_univ_lt u v g
-    | (u,Le,v) -> enforce_univ_leq u v g
-    | (u,Eq,v) -> enforce_univ_eq u v g
-      
 let pr_constraint_type op = 
   let op_str = match op with
     | Lt -> " < "
@@ -1276,8 +715,6 @@ end
 let empty_constraint = Constraint.empty
 let union_constraint = Constraint.union
 let eq_constraint = Constraint.equal
-let merge_constraints c g =
-  Constraint.fold enforce_constraint c g
 
 type constraints = Constraint.t
 
@@ -1378,218 +815,12 @@ let enforce_leq u v c =
 let enforce_leq_level u v c =
   if Level.equal u v then c else Constraint.add (u,Le,v) c
 
-let check_constraint g (l,d,r) =
-  match d with
-  | Eq -> check_equal g l r
-  | Le -> check_smaller g false l r
-  | Lt -> check_smaller g true l r
-
-let check_constraints c g =
-  Constraint.for_all (check_constraint g) c
-
 let enforce_univ_constraint (u,d,v) =
   match d with
   | Eq -> enforce_eq u v
   | Le -> enforce_leq u v
   | Lt -> enforce_leq (super u) v
 
-(* Normalization *)
-
-let lookup_level u g =
-  try Some (UMap.find u g) with Not_found -> None
-
-(** [normalize_universes 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
-    (see the assertion)... I (Stéphane Glondu) am not sure if this
-    plays a role in the rest of the module. *)
-let normalize_universes g =
-  let rec visit u arc cache = match lookup_level u cache with
-    | Some x -> x, cache
-    | None -> match Lazy.force arc with
-    | None ->
-      u, UMap.add u u cache
-    | Some (Canonical {univ=v; lt=_; le=_}) ->
-      v, UMap.add u v cache
-    | Some (Equiv v) ->
-      let v, cache = visit v (lazy (lookup_level v g)) cache in
-      v, UMap.add u v cache
-  in
-  let cache = UMap.fold
-    (fun u arc cache -> snd (visit u (Lazy.lazy_from_val (Some arc)) cache))
-    g UMap.empty
-  in
-  let repr x = UMap.find x cache in
-  let lrepr us = List.fold_left
-    (fun e x -> LSet.add (repr x) e) LSet.empty us
-  in
-  let canonicalize u = function
-    | Equiv _ -> Equiv (repr u)
-    | Canonical {univ=v; lt=lt; le=le; rank=rank} ->
-      assert (u == v);
-      (* avoid duplicates and self-loops *)
-      let lt = lrepr lt and le = lrepr le in
-      let le = LSet.filter
-        (fun x -> x != u && not (LSet.mem x lt)) le
-      in
-      LSet.iter (fun x -> assert (x != u)) lt;
-      Canonical {
-        univ = v;
-        lt = LSet.elements lt;
-        le = LSet.elements le;
-	rank = rank;
-	status = Unset;
-      }
-  in
-  UMap.mapi canonicalize g
-
-let constraints_of_universes g =
-  let constraints_of u v acc =
-    match v with
-    | Canonical {univ=u; lt=lt; le=le} ->
-      let acc = List.fold_left (fun acc v -> Constraint.add (u,Lt,v) acc) acc lt in
-      let acc = List.fold_left (fun acc v -> Constraint.add (u,Le,v) acc) acc le in
-	acc
-    | Equiv v -> Constraint.add (u,Eq,v) acc
-  in
-  UMap.fold constraints_of g Constraint.empty
-
-let constraints_of_universes g =
-  constraints_of_universes (normalize_universes g)
-
-(** Longest path algorithm. This is used to compute the minimal number of
-    universes required if the only strict edge would be the Lt one. This
-    algorithm assumes that the given universes constraints are a almost DAG, in
-    the sense that there may be {Eq, Le}-cycles. This is OK for consistent
-    universes, which is the only case where we use this algorithm. *)
-
-(** Adjacency graph *)
-type graph = constraint_type LMap.t LMap.t
-
-exception Connected
-
-(** Check connectedness *)
-let connected x y (g : graph) =
-  let rec connected x target seen g =
-    if Level.equal x target then raise Connected
-    else if not (LSet.mem x seen) then
-      let seen = LSet.add x seen in
-      let fold z _ seen = connected z target seen g in
-      let neighbours = try LMap.find x g with Not_found -> LMap.empty in
-      LMap.fold fold neighbours seen
-    else seen
-  in
-  try ignore(connected x y LSet.empty g); false with Connected -> true
-
-let add_edge x y v (g : graph) =
-  try
-    let neighbours = LMap.find x g in
-    let neighbours = LMap.add y v neighbours in
-    LMap.add x neighbours g
-  with Not_found ->
-    LMap.add x (LMap.singleton y v) g
-
-(** We want to keep the graph DAG. If adding an edge would cause a cycle, that
-    would necessarily be an {Eq, Le}-cycle, otherwise there would have been a
-    universe inconsistency. Therefore we may omit adding such a cycling edge
-    without changing the compacted graph. *)
-let add_eq_edge x y v g = if connected y x g then g else add_edge x y v g
-
-(** Construct the DAG and its inverse at the same time. *)
-let make_graph g : (graph * graph) =
-  let fold u arc accu = match arc with
-  | Equiv v ->
-    let (dir, rev) = accu in
-    (add_eq_edge u v Eq dir, add_eq_edge v u Eq rev)
-  | Canonical { univ; lt; le; } ->
-    let () = assert (u == univ) in
-    let fold_lt (dir, rev) v = (add_edge u v Lt dir, add_edge v u Lt rev) in
-    let fold_le (dir, rev) v = (add_eq_edge u v Le dir, add_eq_edge v u Le rev) in
-    (** Order is important : lt after le, because of the possible redundancy
-        between [le] and [lt] in a canonical arc. This way, the [lt] constraint
-        is the last one set, which is correct because it implies [le]. *)
-    let accu = List.fold_left fold_le accu le in
-    let accu = List.fold_left fold_lt accu lt in
-    accu
-  in
-  UMap.fold fold g (LMap.empty, LMap.empty)
-
-(** Construct a topological order out of a DAG. *)
-let rec topological_fold u g rem seen accu =
-  let is_seen =
-    try
-      let status = LMap.find u seen in
-      assert status; (** If false, not a DAG! *)
-      true
-    with Not_found -> false
-  in
-  if not is_seen then
-    let rem = LMap.remove u rem in
-    let seen = LMap.add u false seen in
-    let neighbours = try LMap.find u g with Not_found -> LMap.empty in
-    let fold v _ (rem, seen, accu) = topological_fold v g rem seen accu in
-    let (rem, seen, accu) = LMap.fold fold neighbours (rem, seen, accu) in
-    (rem, LMap.add u true seen, u :: accu)
-  else (rem, seen, accu)
-
-let rec topological g rem seen accu =
-  let node = try Some (LMap.choose rem) with Not_found -> None in
-  match node with
-  | None -> accu
-  | Some (u, _) ->
-    let rem, seen, accu = topological_fold u g rem seen accu in
-    topological g rem seen accu
-
-(** Compute the longest path from any vertex. *)
-let constraint_cost = function
-| Eq | Le -> 0
-| Lt -> 1
-
-(** This algorithm browses the graph in topological order, computing for each
-    encountered node the length of the longest path leading to it. Should be
-    O(|V|) or so (modulo map representation). *)
-let rec flatten_graph rem (rev : graph) map mx = match rem with
-| [] -> map, mx
-| u :: rem ->
-  let prev = try LMap.find u rev with Not_found -> LMap.empty in
-  let fold v cstr accu =
-    let v_cost = LMap.find v map in
-    max (v_cost + constraint_cost cstr) accu
-  in
-  let u_cost = LMap.fold fold prev 0 in
-  let map = LMap.add u u_cost map in
-  flatten_graph rem rev map (max mx u_cost)
-
-(** [sort_universes g] builds a map from universes in [g] to natural
-    numbers. It outputs a graph containing equivalence edges from each
-    level appearing in [g] to [Type.n], and [lt] edges between the
-    [Type.n]s. The output graph should imply the input graph (and the
-    [Type.n]s. The output graph should imply the input graph (and the
-    implication will be strict most of the time), but is not
-    necessarily minimal. 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_universes orig =
-  let (dir, rev) = make_graph orig in
-  let order = topological dir dir LMap.empty [] in
-  let compact, max = flatten_graph order rev LMap.empty 0 in
-  let mp = Names.DirPath.make [Names.Id.of_string "Type"] in
-  let types = Array.init (max + 1) (fun n -> Level.make mp n) in
-  (** Old universes are made equal to [Type.n] *)
-  let fold u level accu = UMap.add u (Equiv types.(level)) accu in
-  let sorted = LMap.fold fold compact UMap.empty in
-  (** Add all [Type.n] nodes *)
-  let fold i accu u =
-    if i < max then
-      let pred = types.(i + 1) in
-      let arc = {univ = u; lt = [pred]; le = []; rank = 0; status = Unset; } in
-      UMap.add u (Canonical arc) accu
-    else accu
-  in
-  Array.fold_left_i fold sorted types
-
 (* Miscellaneous functions to remove or test local univ assumed to
    occur in a universe *)
 
@@ -1645,7 +876,6 @@ module Instance : sig
     
     val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds
     val levels : t -> LSet.t
-    val check_eq : t check_function 
 end = 
 struct
   type t = Level.t array
@@ -1729,13 +959,6 @@ struct
 	 (* Necessary as universe instances might come from different modules and 
 	    unmarshalling doesn't preserve sharing *))
 
-  let check_eq g t1 t2 =
-    t1 == t2 ||
-      (Int.equal (Array.length t1) (Array.length t2) &&
-	 let rec aux i =
-	   (Int.equal i (Array.length t1)) || (check_eq_level g t1.(i) t2.(i) && aux (i + 1))
-	 in aux 0)
-
 end
 
 let enforce_eq_instances x y = 
@@ -1985,27 +1208,6 @@ let abstract_universes poly ctx =
 
 (** Pretty-printing *)
 
-let pr_arc prl = function
-  | _, Canonical {univ=u; lt=[]; le=[]} ->
-      mt ()
-  | _, Canonical {univ=u; lt=lt; le=le} ->
-      let opt_sep = match lt, le with
-      | [], _ | _, [] -> mt ()
-      | _ -> spc ()
-      in
-      prl u ++ str " " ++
-      v 0
-        (pr_sequence (fun v -> str "< " ++ prl v) lt ++
-	 opt_sep ++
-         pr_sequence (fun v -> str "<= " ++ prl v) le) ++
-      fnl ()
-  | u, Equiv v ->
-      prl u  ++ str " = " ++ prl v ++ fnl ()
-
-let pr_universes prl g =
-  let graph = UMap.fold (fun u a l -> (u,a)::l) g [] in
-  prlist (pr_arc prl) graph
-
 let pr_constraints prl = Constraint.pr prl
 
 let pr_universe_context = UContext.pr
@@ -2018,19 +1220,6 @@ let pr_universe_subst =
 let pr_universe_level_subst = 
   LMap.pr (fun u -> str" := " ++ Level.pr u ++ spc ())
 
-(* Dumping constraints to a file *)
-
-let dump_universes output g =
-  let dump_arc u = function
-    | Canonical {univ=u; lt=lt; le=le} ->
-	let u_str = Level.to_string u in
-	List.iter (fun v -> output Lt (Level.to_string v) u_str) lt;
-	List.iter (fun v -> output Le (Level.to_string v) u_str) le
-    | Equiv v ->
-      output Eq (Level.to_string u) (Level.to_string v)
-  in
-  UMap.iter dump_arc g
-
 module Huniverse_set = 
   Hashcons.Make(
     struct
@@ -2078,26 +1267,3 @@ let subst_instance_constraints =
     let key = Profile.declare_profile "subst_instance_constraints" in
       Profile.profile2 key subst_instance_constraints
   else subst_instance_constraints
-
-let merge_constraints = 
-  if Flags.profile then 
-    let key = Profile.declare_profile "merge_constraints" in
-      Profile.profile2 key merge_constraints
-  else merge_constraints
-let check_constraints =
-  if Flags.profile then
-    let key = Profile.declare_profile "check_constraints" in
-      Profile.profile2 key check_constraints
-  else check_constraints
-
-let check_eq = 
-  if Flags.profile then
-    let check_eq_key = Profile.declare_profile "check_eq" in
-      Profile.profile3 check_eq_key check_eq
-  else check_eq
-
-let check_leq = 
-  if Flags.profile then 
-    let check_leq_key = Profile.declare_profile "check_leq" in
-      Profile.profile3 check_leq_key check_leq
-  else check_leq
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 4cc8a2528..dbbc83262 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -40,6 +40,9 @@ sig
   val pr : t -> Pp.std_ppcmds
   (** Pretty-printing *)
 
+  val to_string : t -> string
+  (** Debug printing *)
+
   val var : int -> t
 
   val var_index : t -> int option
@@ -115,6 +118,9 @@ sig
   
   val type1 : t 
   (** the universe of the type of Prop/Set *)
+
+  val exists : (Level.t * int -> bool) -> t -> bool
+  val for_all : (Level.t * int -> bool) -> t -> bool
 end
 
 type universe = Universe.t
@@ -148,31 +154,6 @@ val univ_level_mem : universe_level -> universe -> bool
 
 val univ_level_rem : universe_level -> universe -> universe -> universe
 
-(** {6 Graphs of universes. } *)
-
-type universes
-
-type 'a check_function = universes -> 'a -> 'a -> bool
-val check_leq : universe check_function
-val check_eq : universe check_function
-
-(** The empty graph of universes *)
-val empty_universes : universes
-
-(** The initial graph of universes: Prop < Set *)
-val initial_universes : universes
-
-val is_initial_universes : universes -> bool
-
-val sort_universes : universes -> universes
-
-(** Adds a universe to the graph, ensuring it is >= or > Set.
-   @raises AlreadyDeclared if the level is already declared in the graph. *)
-
-exception AlreadyDeclared
-
-val add_universe : universe_level -> bool -> universes -> universes
-
 (** {6 Constraints. } *)
 
 type constraint_type = Lt | Le | Eq
@@ -203,12 +184,6 @@ val enforce_leq : universe constraint_function
 val enforce_eq_level : universe_level constraint_function
 val enforce_leq_level : universe_level constraint_function
 
-(** {6 ... } *)
-(** Merge of constraints in a universes graph.
-  The function [merge_constraints] merges a set of constraints in a given
-  universes graph. It raises the exception [UniverseInconsistency] if the
-  constraints are not satisfiable. *)
-
 (** Type explanation is used to decorate error messages to provide
   useful explanation why a given constraint is rejected. It is composed
   of a path of universes and relation kinds [(r1,u1);..;(rn,un)] means
@@ -226,14 +201,6 @@ type univ_inconsistency = constraint_type * universe * universe * explanation op
 
 exception UniverseInconsistency of univ_inconsistency
 
-val enforce_constraint : univ_constraint -> universes -> universes
-val merge_constraints : constraints -> universes -> universes
-
-val constraints_of_universes : universes -> constraints
-
-val check_constraint  : universes -> univ_constraint -> bool
-val check_constraints : constraints -> universes -> bool
-
 (** {6 Support for universe polymorphism } *)
 
 (** Polymorphic maps from universe levels to 'a *)
@@ -309,8 +276,6 @@ sig
   val levels : t -> LSet.t
   (** The set of levels in the instance *)
 
-  val check_eq : t check_function 
-  (** Check equality of instances w.r.t. a universe graph *)
 end
 
 type universe_instance = Instance.t
@@ -424,7 +389,6 @@ val instantiate_univ_constraints : universe_instance -> universe_context -> cons
 
 (** {6 Pretty-printing of universes. } *)
 
-val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds
 val pr_constraint_type : constraint_type -> Pp.std_ppcmds
 val pr_constraints : (Level.t -> Pp.std_ppcmds) -> constraints -> Pp.std_ppcmds
 val pr_universe_context : (Level.t -> Pp.std_ppcmds) -> universe_context -> Pp.std_ppcmds
@@ -435,12 +399,6 @@ val explain_universe_inconsistency : (Level.t -> Pp.std_ppcmds) ->
 val pr_universe_level_subst : universe_level_subst -> Pp.std_ppcmds
 val pr_universe_subst : universe_subst -> Pp.std_ppcmds
 
-(** {6 Dumping to a file } *)
-
-val dump_universes :
-  (constraint_type -> string -> string -> unit) ->
-  universes -> unit
-
 (** {6 Hash-consing } *)
 
 val hcons_univ : universe -> universe
diff --git a/library/global.mli b/library/global.mli
index ac231f7fd..455751d41 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -19,7 +19,7 @@ val env : unit -> Environ.env
 
 val env_is_initial : unit -> bool
 
-val universes : unit -> Univ.universes
+val universes : unit -> UGraph.t
 val named_context_val : unit -> Environ.named_context_val
 val named_context : unit -> Context.named_context
 
diff --git a/library/universes.ml b/library/universes.ml
index bc42cc044..067558c8a 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -113,7 +113,7 @@ let to_constraints g s =
       | _, ULe, Some l' -> enforce_leq x y acc
       | _, ULub, _ -> acc
       | _, d, _ -> 
-	let f = if d == ULe then check_leq else check_eq in
+	let f = if d == ULe then UGraph.check_leq else UGraph.check_eq in
 	  if f g x y then acc else 
 	    raise (Invalid_argument 
 		   "to_constraints: non-trivial algebraic constraint between universes")
@@ -123,12 +123,12 @@ let eq_constr_univs_infer univs m n =
   if m == n then true, Constraints.empty
   else 
     let cstrs = ref Constraints.empty in
-    let eq_universes strict = Univ.Instance.check_eq univs in
+    let eq_universes strict = UGraph.check_eq_instances univs in
     let eq_sorts s1 s2 = 
       if Sorts.equal s1 s2 then true
       else
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	  if Univ.check_eq univs u1 u2 then true
+	  if UGraph.check_eq univs u1 u2 then true
 	  else
 	    (cstrs := Constraints.add (u1, UEq, u2) !cstrs;
 	     true)
@@ -149,12 +149,12 @@ let eq_constr_univs_infer_with kind1 kind2 univs m n =
      [kind1,kind2], because [kind1] and [kind2] may be different,
      typically evaluating [m] and [n] in different evar maps. *)
   let cstrs = ref Constraints.empty in
-  let eq_universes strict = Univ.Instance.check_eq univs in
+  let eq_universes strict = UGraph.check_eq_instances univs in
   let eq_sorts s1 s2 = 
     if Sorts.equal s1 s2 then true
     else
       let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-      if Univ.check_eq univs u1 u2 then true
+      if UGraph.check_eq univs u1 u2 then true
       else
 	(cstrs := Constraints.add (u1, UEq, u2) !cstrs;
 	 true)
@@ -169,12 +169,12 @@ let leq_constr_univs_infer univs m n =
   if m == n then true, Constraints.empty
   else 
     let cstrs = ref Constraints.empty in
-    let eq_universes strict l l' = Univ.Instance.check_eq univs l l' in
+    let eq_universes strict l l' = UGraph.check_eq_instances univs l l' in
     let eq_sorts s1 s2 = 
       if Sorts.equal s1 s2 then true
       else
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	if Univ.check_eq univs u1 u2 then true
+	if UGraph.check_eq univs u1 u2 then true
 	else (cstrs := Constraints.add (u1, UEq, u2) !cstrs;
 	      true)
     in
@@ -182,7 +182,7 @@ let leq_constr_univs_infer univs m n =
       if Sorts.equal s1 s2 then true
       else 
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	  if Univ.check_leq univs u1 u2 then
+	  if UGraph.check_leq univs u1 u2 then
 	    ((if Univ.is_small_univ u1 then
 		cstrs := Constraints.add (u1, ULe, u2) !cstrs);
 	     true)
@@ -845,27 +845,27 @@ let normalize_context_set ctx us algs =
   let csts = 
     (* We first put constraints in a normal-form: all self-loops are collapsed
        to equalities. *)
-    let g = Univ.LSet.fold (fun v g -> Univ.add_universe v false g)
-			   ctx Univ.empty_universes
+    let g = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g)
+			   ctx UGraph.empty_universes
     in
     let g =
       Univ.Constraint.fold
 	(fun (l, d, r) g ->
 	 let g =
 	   if not (Level.is_small l || LSet.mem l ctx) then
-	     try Univ.add_universe l false g
-	     with Univ.AlreadyDeclared -> g
+	     try UGraph.add_universe l false g
+	     with UGraph.AlreadyDeclared -> g
 	   else g
 	 in
 	 let g =
 	   if not (Level.is_small r || LSet.mem r ctx) then
-	     try Univ.add_universe r false g
-	     with Univ.AlreadyDeclared -> g
+	     try UGraph.add_universe r false g
+	     with UGraph.AlreadyDeclared -> g
 	   else g
 	 in g) csts g
     in
-    let g = Univ.Constraint.fold Univ.enforce_constraint csts g in
-      Univ.constraints_of_universes g
+    let g = Univ.Constraint.fold UGraph.enforce_constraint csts g in
+      UGraph.constraints_of_universes g
   in
   let noneqs =
     Constraint.fold (fun (l,d,r as cstr) noneqs ->
@@ -995,7 +995,7 @@ let refresh_constraints univs (ctx, cstrs) =
     Univ.Constraint.fold (fun c (cstrs', univs as acc) -> 
       let c = translate_cstr c in
       if is_trivial_leq c then acc
-      else (Univ.Constraint.add c cstrs', Univ.enforce_constraint c univs))
+      else (Univ.Constraint.add c cstrs', UGraph.enforce_constraint c univs))
       cstrs (Univ.Constraint.empty, univs)
   in ((ctx, cstrs'), univs')
 
diff --git a/library/universes.mli b/library/universes.mli
index 5527da090..c897a88a9 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -60,11 +60,11 @@ val subst_univs_universe_constraints : universe_subst_fn ->
 
 val enforce_eq_instances_univs : bool -> universe_instance universe_constraint_function
 
-val to_constraints : universes -> universe_constraints -> constraints
+val to_constraints : UGraph.t -> universe_constraints -> constraints
 
 (** [eq_constr_univs_infer u a b] is [true, c] if [a] equals [b] modulo alpha, casts,
    application grouping, the universe constraints in [u] and additional constraints [c]. *)
-val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained
+val eq_constr_univs_infer : UGraph.t -> constr -> constr -> bool universe_constrained
 
 (** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of
     {!eq_constr_univs_infer} taking kind-of-term functions, to expose
@@ -72,12 +72,12 @@ val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_
 val eq_constr_univs_infer_with :
   (constr -> (constr,types) kind_of_term) ->
   (constr -> (constr,types) kind_of_term) ->
-  Univ.universes -> constr -> constr -> bool universe_constrained
+  UGraph.t -> constr -> constr -> bool universe_constrained
 
 (** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b]
     modulo alpha, casts, application grouping, the universe constraints
     in [u] and additional constraints [c]. *)
-val leq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained
+val leq_constr_univs_infer : UGraph.t -> constr -> constr -> bool universe_constrained
 
 (** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
     application grouping and the universe constraints in [c]. *)
@@ -212,7 +212,7 @@ val restrict_universe_context : universe_context_set -> universe_set -> universe
 val simplify_universe_context : universe_context_set -> 
   universe_context_set * universe_level_subst
 
-val refresh_constraints : universes -> universe_context_set -> universe_context_set * universes
+val refresh_constraints : UGraph.t -> universe_context_set -> universe_context_set * UGraph.t
 
 (** Pretty-printing *)
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2efd8fe41..6373e6079 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -111,7 +111,7 @@ let interp_universe_level_name evd s =
 	 let level = Univ.Level.make dp num in
 	 let evd =
 	   try Evd.add_global_univ evd level
-	   with Univ.AlreadyDeclared -> evd
+	   with UGraph.AlreadyDeclared -> evd
 	 in evd, level
     else 
       try
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 1df2a73b2..5e1c467c8 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -251,7 +251,7 @@ type conversion_test = constraints -> constraints
 val pb_is_equal : conv_pb -> bool
 val pb_equal : conv_pb -> conv_pb
 
-val sort_cmp : env -> conv_pb -> sorts -> sorts -> universes -> unit
+val sort_cmp : env -> conv_pb -> sorts -> sorts -> UGraph.t -> unit
 
 val is_conv : env ->  evar_map -> constr -> constr -> bool
 val is_conv_leq : env ->  evar_map -> constr -> constr -> bool
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c07c756c0..229f3acfd 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -347,7 +347,7 @@ let dump_universes_gen g s =
     end
   in
   try
-    Univ.dump_universes output_constraint g;
+    UGraph.dump_universes output_constraint g;
     close ();
     msg_info (str "Universes written to file \"" ++ str s ++ str "\".")
   with reraise ->
@@ -357,7 +357,7 @@ let dump_universes_gen g s =
 
 let dump_universes sorted s =
   let g = Global.universes () in
-  let g = if sorted then Univ.sort_universes g else g in
+  let g = if sorted then UGraph.sort_universes g else g in
   dump_universes_gen g s
 
 (*********************)
@@ -1640,12 +1640,12 @@ let vernac_print = function
   | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections ())
   | PrintUniverses (b, None) ->
      let univ = Global.universes () in
-     let univ = if b then Univ.sort_universes univ else univ in
+     let univ = if b then UGraph.sort_universes univ else univ in
      let pr_remaining =
        if Global.is_joined_environment () then mt ()
        else str"There may remain asynchronous universe constraints"
      in
-     msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining)
+     msg_notice (UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining)
   | PrintUniverses (b, Some s) -> dump_universes b s
   | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r))
   | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ())