Dedicated file for universe unification context manipulation.

This allows to remove a lot of independent code from Evd which was put
into the UState module. The API is not perfect yet, but this is a first
pass. Names of data structures should be thought about too because they
are way too similar.

1 files changed, 53 insertions, 475 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 79e73bda5..cfe9a3da4 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -259,221 +259,20 @@ let instantiate_evar_array info c args =
   | [] -> c
   | _ -> replace_vars inst c
 
-module StringOrd = struct type t = string let compare = String.compare end
-module UNameMap = struct
-    
-  include Map.Make(StringOrd)
-    
-  let union s t = 
-    if s == t then s
-    else
-      merge (fun k l r -> 
-	match l, r with
-	| Some _, _ -> l
-	| _, _ -> r) s t
-end
-
-(* 2nd part used to check consistency on the fly. *)
-type evar_universe_context = 
- { uctx_names : Univ.Level.t UNameMap.t * string Univ.LMap.t;
-   uctx_local : Univ.universe_context_set; (** The local context of variables *)
-   uctx_univ_variables : Universes.universe_opt_subst;
-   (** The local universes that are unification variables *)
-   uctx_univ_algebraic : Univ.universe_set; 
-   (** The subset of unification variables that
-	can be instantiated with algebraic universes as they appear in types 
-	and universe instances only. *)
-   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 = 
-  { uctx_names = UNameMap.empty, Univ.LMap.empty;
-    uctx_local = Univ.ContextSet.empty;
-    uctx_univ_variables = Univ.LMap.empty;
-    uctx_univ_algebraic = Univ.LSet.empty;
-    uctx_universes = UGraph.initial_universes;
-    uctx_initial_universes = UGraph.initial_universes }
-
-let evar_universe_context_from e = 
-  let u = universes e in
-    {empty_evar_universe_context with 
-      uctx_universes = u; uctx_initial_universes = u}
-
-let is_empty_evar_universe_context ctx =
-  Univ.ContextSet.is_empty ctx.uctx_local && 
-    Univ.LMap.is_empty ctx.uctx_univ_variables
-
-let union_evar_universe_context ctx ctx' =
-  if ctx == ctx' then ctx
-  else if is_empty_evar_universe_context ctx' then ctx
-  else
-    let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in
-    let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in
-    let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local)
-			       (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 -> 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);
-	uctx_local = local;
-	uctx_univ_variables = 
-	  Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables;
-	uctx_univ_algebraic = 
-	  Univ.LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic;
-	uctx_initial_universes = declarenew ctx.uctx_initial_universes;
-	uctx_universes = 
-	  if local == ctx.uctx_local then ctx.uctx_universes
-	  else
-	    let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in
-	      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 =  *)
-(*   Profile.profile2 union_evar_universe_context_key union_evar_universe_context;; *)
-
+type evar_universe_context = UState.t
 type 'a in_evar_universe_context = 'a * evar_universe_context
 
-let evar_universe_context_set diff ctx =
-  let initctx = ctx.uctx_local in
-  let cstrs =
-    Univ.LSet.fold
-      (fun l cstrs ->
-       try
-	 match Univ.LMap.find l ctx.uctx_univ_variables with
-	 | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs
-	 | None -> cstrs
-       with Not_found | Option.IsNone -> cstrs)
-      (Univ.Instance.levels (Univ.UContext.instance diff)) Univ.Constraint.empty
-  in
-    Univ.ContextSet.add_constraints cstrs initctx 
-		      
-let evar_universe_context_constraints ctx = snd ctx.uctx_local
-let evar_context_universe_context ctx = Univ.ContextSet.to_context ctx.uctx_local
-    
-let evar_universe_context_of ctx = { empty_evar_universe_context with uctx_local = ctx }
-let evar_universe_context_subst ctx = ctx.uctx_univ_variables
-
-let instantiate_variable l b v =
-  v := Univ.LMap.add l (Some b) !v
-
-exception UniversesDiffer
-
-let process_universe_constraints univs vars alg cstrs =
-  let vars = ref vars in
-  let normalize = Universes.normalize_universe_opt_subst vars in
-  let rec unify_universes fo l d r local =
-    let l = normalize l and r = normalize r in
-      if Univ.Universe.equal l r then local
-      else 
-	let varinfo x = 
-	  match Univ.Universe.level x with
-	  | None -> Inl x
-	  | Some l -> Inr (l, Univ.LMap.mem l !vars, Univ.LSet.mem l alg)
-	in
-	  if d == Universes.ULe 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 
-		match Univ.Universe.level r with
-		| Some r ->
-		  Univ.Constraint.add (Option.get (Univ.Universe.level l),Univ.Le,r) local
-		| _ -> local
-	      else local
-	    else
-	      match Univ.Universe.level r with
-	      | None -> error ("Algebraic universe on the right")
-	      | Some rl ->
-		if Univ.Level.is_small rl then
-		  let levels = Univ.Universe.levels l in
-		    Univ.LSet.fold (fun l local ->
-		      if Univ.Level.is_small l || Univ.LMap.mem l !vars then
-			unify_universes fo (Univ.Universe.make l) Universes.UEq r local
-		      else raise (Univ.UniverseInconsistency (Univ.Le, Univ.Universe.make l, r, None)))
-		      levels local
-		else
-		  Univ.enforce_leq l r local
-	  else if d == Universes.ULub then
-	    match varinfo l, varinfo r with
-	    | (Inr (l, true, _), Inr (r, _, _)) 
-	    | (Inr (r, _, _), Inr (l, true, _)) -> 
-	      instantiate_variable l (Univ.Universe.make r) vars; 
-	      Univ.enforce_eq_level l r local
-	    | Inr (_, _, _), Inr (_, _, _) ->
-	      unify_universes true l Universes.UEq r local
-	    | _, _ -> assert false
-	  else (* d = Universes.UEq *)
-	    match varinfo l, varinfo r with
-	    | Inr (l', lloc, _), Inr (r', rloc, _) ->
-	      let () = 
-		if lloc then
-		  instantiate_variable l' r vars
-		else if rloc then 
-		  instantiate_variable r' l vars
-		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
-		    raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
-		  else
-		    if fo then 
-		      raise UniversesDiffer
-	      in
-	        Univ.enforce_eq_level l' r' local
-	    | Inr (l, loc, alg), Inl r
-	    | Inl r, Inr (l, loc, alg) ->
-	       let inst = Univ.univ_level_rem l r r in
-		 if alg then (instantiate_variable l inst vars; local)
-		 else
-		   let lu = Univ.Universe.make l in
-		   if Univ.univ_level_mem l r then
-		     Univ.enforce_leq inst lu local
-		   else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None))
-            | _, _ (* One of the two is algebraic or global *) -> 
-	     if UGraph.check_eq univs l r then local
-	     else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
-  in
-  let local = 
-    Universes.Constraints.fold (fun (l,d,r) local -> unify_universes false l d r local)
-      cstrs Univ.Constraint.empty
-  in
-    !vars, local
-
-let add_constraints_context ctx cstrs =
-  let univs, local = ctx.uctx_local in
-  let cstrs' = Univ.Constraint.fold (fun (l,d,r) acc -> 
-    let l = Univ.Universe.make l and r = Univ.Universe.make r in
-    let cstr' = 
-      if d == Univ.Lt then (Univ.Universe.super l, Universes.ULe, r)
-      else (l, (if d == Univ.Le then Universes.ULe else Universes.UEq), r)
-    in Universes.Constraints.add cstr' acc)
-    cstrs Universes.Constraints.empty
-  in
-  let vars, local' =
-    process_universe_constraints ctx.uctx_universes
-      ctx.uctx_univ_variables ctx.uctx_univ_algebraic
-      cstrs'
-  in
-    { ctx with uctx_local = (univs, Univ.Constraint.union local local');
-      uctx_univ_variables = vars;
-      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;; *)
-
-let add_universe_constraints_context ctx cstrs =
-  let univs, local = ctx.uctx_local in
-  let vars, local' = 
-    process_universe_constraints ctx.uctx_universes 
-      ctx.uctx_univ_variables ctx.uctx_univ_algebraic 
-      cstrs 
-  in
-    { ctx with uctx_local = (univs, Univ.Constraint.union local local');
-      uctx_univ_variables = vars;
-      uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes }
+let empty_evar_universe_context = UState.empty
+let evar_universe_context_from = UState.from
+let is_empty_evar_universe_context = UState.is_empty
+let union_evar_universe_context = UState.union
+let evar_universe_context_set = UState.context_set
+let evar_universe_context_constraints = UState.constraints
+let evar_context_universe_context = UState.context
+let evar_universe_context_of = UState.of_context_set
+let evar_universe_context_subst = UState.subst
+let add_constraints_context = UState.add_constraints
+let add_universe_constraints_context = UState.add_universe_constraints
 
 (* let addunivconstrkey = Profile.declare_profile "add_universe_constraints_context";; *)
 (* let add_universe_constraints_context =  *)
@@ -937,7 +736,7 @@ let evars_of_filtered_evar_info evi =
 (**********************************************************)
 (* Sort variables *)
 
-type rigid = 
+type rigid = UState.rigid =
   | UnivRigid
   | UnivFlexible of bool (** Is substitution by an algebraic ok? *)
 
@@ -947,146 +746,32 @@ let univ_flexible_alg = UnivFlexible true
 
 let evar_universe_context d = d.universes
 
-let universe_context_set d = d.universes.uctx_local
-
-let pr_uctx_level uctx = 
-  let map, map_rev = uctx.uctx_names in 
-    fun l ->
-      try str(Univ.LMap.find l map_rev)
-      with Not_found -> 
-	Universes.pr_with_global_universes l
-
-let universe_context ?names evd =
-  match names with
-  | None -> Univ.ContextSet.to_context evd.universes.uctx_local
-  | Some pl ->
-     let levels = Univ.ContextSet.levels evd.universes.uctx_local in
-     let newinst, left =
-       List.fold_right
-         (fun (loc,id) (newinst, acc) ->
-	  let l =
-	    try UNameMap.find (Id.to_string id) (fst evd.universes.uctx_names)
-	    with Not_found ->
-	      user_err_loc (loc, "universe_context",
-			    str"Universe " ++ pr_id id ++ str" is not bound anymore.")
-	  in (l :: newinst, Univ.LSet.remove l acc))
-	 pl ([], levels)
-     in
-       if not (Univ.LSet.is_empty left) then
-         let n = Univ.LSet.cardinal left in
-           errorlabstrm "universe_context"
-			(str(CString.plural n "Universe") ++ spc () ++
-			     Univ.LSet.pr (pr_uctx_level evd.universes) left ++
-			     spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.")
-       else Univ.UContext.make (Univ.Instance.of_array (Array.of_list newinst),
-				Univ.ContextSet.constraints evd.universes.uctx_local)
+let universe_context_set d = UState.context_set Univ.UContext.empty d.universes
+
+let pr_uctx_level = UState.pr_uctx_level
+let universe_context ?names evd = UState.universe_context ?names evd.universes
 
 let restrict_universe_context evd vars =
-  let uctx = evd.universes in
-  let uctx' = Universes.restrict_universe_context uctx.uctx_local vars in
-    { evd with universes = { uctx with uctx_local = uctx' } }
-						 
+  { evd with universes = UState.restrict evd.universes vars }
+
 let universe_subst evd =
-  evd.universes.uctx_univ_variables
-
-let merge_uctx sideff rigid uctx ctx' =
-  let open Univ in
-  let levels = ContextSet.levels ctx' in
-  let uctx = if sideff then uctx else
-    match rigid with
-    | UnivRigid -> uctx
-    | UnivFlexible b ->
-      let fold u accu =
-        if LMap.mem u accu then accu
-        else LMap.add u None accu
-      in
-      let uvars' = LSet.fold fold levels uctx.uctx_univ_variables in
-	if b then
-	  { uctx with uctx_univ_variables = uvars';
-	  uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels }
-	else { uctx with uctx_univ_variables = uvars' }
-  in
-  let uctx_local =
-    if sideff then uctx.uctx_local
-    else ContextSet.append ctx' uctx.uctx_local
-  in
-  let declare g =
-    LSet.fold (fun u 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 = UGraph.merge_constraints (ContextSet.constraints ctx') univs in
-    { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial }
+  UState.subst evd.universes
 
 let merge_context_set ?(sideff=false) rigid evd ctx' = 
-  {evd with universes = merge_uctx sideff rigid evd.universes ctx'}
+  {evd with universes = UState.merge sideff rigid evd.universes ctx'}
 
-let merge_uctx_subst uctx s =
-  { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s }
-      
 let merge_universe_subst evd subst = 
-  {evd with universes = merge_uctx_subst evd.universes subst }
+  {evd with universes = UState.merge_subst evd.universes subst }
 
 let with_context_set rigid d (a, ctx) = 
   (merge_context_set rigid d ctx, a)
 
-let emit_universe_side_effects eff u =
-  Declareops.fold_side_effects
-    (fun acc eff ->
-     match eff with
-     | Declarations.SEscheme (l,s) ->
-	List.fold_left
-	  (fun acc (_,_,cb,c) ->
-	   let acc = match c with
-	     | `Nothing -> acc
-	     | `Opaque (s, ctx) -> merge_uctx true univ_rigid acc ctx
-	   in if cb.Declarations.const_polymorphic then acc
-	      else
-		merge_uctx true univ_rigid acc
-			   (Univ.ContextSet.of_context cb.Declarations.const_universes))
-	  acc l
-     | Declarations.SEsubproof _ -> acc)
-    u eff
-        
-let add_uctx_names s l (names, names_rev) =
-    (UNameMap.add s l names, Univ.LMap.add l s names_rev)
-
-let uctx_new_univ_variable rigid name predicative
-  ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
-  let u = Universes.new_univ_level (Global.current_dirpath ()) in
-  let ctx' = Univ.ContextSet.add_universe u ctx in
-  let uctx', pred =
-    match rigid with
-    | UnivRigid -> uctx, true
-    | UnivFlexible b -> 
-      let uvars' = Univ.LMap.add u None uvars in
-	if b then {uctx with uctx_univ_variables = uvars';
-	  uctx_univ_algebraic = Univ.LSet.add u avars}, false
-	else {uctx with uctx_univ_variables = uvars'}, false
-  in
-  let names = 
-    match name with
-    | Some n -> add_uctx_names n u uctx.uctx_names
-    | None -> uctx.uctx_names
-  in
-  let initial =
-    UGraph.add_universe u false uctx.uctx_initial_universes
-  in						     
-  let uctx' =
-    {uctx' with uctx_names = names; uctx_local = ctx';
-		uctx_universes = UGraph.add_universe u false uctx.uctx_universes;
-		uctx_initial_universes = initial}
-  in uctx', u
-						     
 let new_univ_level_variable ?name ?(predicative=true) rigid evd =
-  let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in
+  let uctx', u = UState.new_univ_variable rigid name evd.universes in
     ({evd with universes = uctx'}, u)
 
 let new_univ_variable ?name ?(predicative=true) rigid evd =
-  let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in
+  let uctx', u = UState.new_univ_variable rigid name evd.universes in
     ({evd with universes = uctx'}, Univ.Universe.make u)
 
 let new_sort_variable ?name ?(predicative=true) rigid d =
@@ -1094,42 +779,12 @@ let new_sort_variable ?name ?(predicative=true) rigid d =
     (d', Type u)
 
 let add_global_univ d u =
-  let uctx = d.universes in
-  let initial =
-    UGraph.add_universe u true uctx.uctx_initial_universes
-  in
-  let univs = 
-    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;
-				     uctx_universes = univs } }
-      
+  { d with universes = UState.add_global_univ d.universes u }
+
 let make_flexible_variable evd b u =
-  let {uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as ctx = evd.universes in
-  let uvars' = Univ.LMap.add u None uvars in
-  let avars' = 
-    if b then
-      let uu = Univ.Universe.make u in
-      let substu_not_alg u' v =
-	Option.cata (fun vu -> Univ.Universe.equal uu vu && not (Univ.LSet.mem u' avars)) false v
-      in
-	if not (Univ.LMap.exists substu_not_alg uvars)
-	then Univ.LSet.add u avars else avars 
-    else avars 
-  in
-    {evd with universes = {ctx with uctx_univ_variables = uvars'; 
-      uctx_univ_algebraic = avars'}}
-
-let make_evar_universe_context e l = 
-  let uctx = evar_universe_context_from e in
-    match l with
-    | None -> uctx
-    | Some us ->
-       List.fold_left
-	 (fun uctx (loc,id) ->
-	  fst (uctx_new_univ_variable univ_rigid (Some (Id.to_string id)) true uctx))
-	 uctx us
+  { evd with universes = UState.make_flexible_variable evd.universes b u }
+
+let make_evar_universe_context = UState.make
     
 (****************************************)
 (* Operations on constants              *)
@@ -1152,20 +807,11 @@ let fresh_global ?(rigid=univ_flexible) ?names env evd gr =
 
 let whd_sort_variable evd t = t
 
-let is_sort_variable evd s = 
-  match s with 
-  | Type u -> 
-    (match Univ.universe_level u with
-    | Some l as x -> 
-      let uctx = evd.universes in
-	if Univ.LSet.mem l (Univ.ContextSet.levels uctx.uctx_local) then x
-	else None
-    | None -> None)
-  | _ -> None
+let is_sort_variable evd s = UState.is_sort_variable evd.universes s
 
 let is_flexible_level evd l = 
   let uctx = evd.universes in
-    Univ.LMap.mem l uctx.uctx_univ_variables
+    Univ.LMap.mem l (UState.subst uctx)
 
 let is_eq_sort s1 s2 =
   if Sorts.equal s1 s2 then None
@@ -1176,12 +822,12 @@ let is_eq_sort s1 s2 =
       else Some (u1, u2)
 
 let normalize_universe evd =
-  let vars = ref evd.universes.uctx_univ_variables in
+  let vars = ref (UState.subst evd.universes) in
   let normalize = Universes.normalize_universe_opt_subst vars in
     normalize
 
 let normalize_universe_instance evd l =
-  let vars = ref evd.universes.uctx_univ_variables in
+  let vars = ref (UState.subst evd.universes) in
   let normalize = Univ.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in
     Univ.Instance.subst_fn normalize l
 
@@ -1239,96 +885,28 @@ let set_leq_sort env evd s1 s2 =
       else evd
 	    
 let check_eq evd s s' =
-  UGraph.check_eq evd.universes.uctx_universes s s'
+  UGraph.check_eq (UState.ugraph evd.universes) s s'
 
 let check_leq evd 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)
+  UGraph.check_leq (UState.ugraph evd.universes) s s'
 
-let normalize_evar_universe_context_variables uctx =
-  let normalized_variables, undef, def, subst = 
-    Universes.normalize_univ_variables uctx.uctx_univ_variables 
-  in
-  let ctx_local = subst_univs_context_with_def def (Univ.make_subst subst) uctx.uctx_local in
-  let ctx_local', univs = Universes.refresh_constraints uctx.uctx_initial_universes ctx_local in
-    subst, { uctx with uctx_local = ctx_local';
-      uctx_univ_variables = normalized_variables;
-      uctx_universes = univs }
+let normalize_evar_universe_context_variables = UState.normalize_variables
 
 (* let normvarsconstrkey = Profile.declare_profile "normalize_evar_universe_context_variables";; *)
 (* let normalize_evar_universe_context_variables = *)
 (*   Profile.profile1 normvarsconstrkey normalize_evar_universe_context_variables;; *)
     
-let abstract_undefined_variables uctx =
-  let vars' = 
-    Univ.LMap.fold (fun u v acc ->
-      if v == None then Univ.LSet.remove u acc
-      else acc)
-    uctx.uctx_univ_variables uctx.uctx_univ_algebraic
-  in { uctx with uctx_local = Univ.ContextSet.empty;
-      uctx_univ_algebraic = vars' }
-
-let fix_undefined_variables ({ universes = uctx } as evm) =
-  let algs', vars' = 
-    Univ.LMap.fold (fun u v (algs, vars as acc) ->
-      if v == None then (Univ.LSet.remove u algs, Univ.LMap.remove u vars)
-      else acc)
-      uctx.uctx_univ_variables 
-      (uctx.uctx_univ_algebraic, uctx.uctx_univ_variables)
-  in
-    {evm with universes = 
-	{ uctx with uctx_univ_variables = vars';
-	  uctx_univ_algebraic = algs' } }
+let abstract_undefined_variables = UState.abstract_undefined_variables
 
-
-let refresh_undefined_univ_variables uctx =
-  let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in
-  let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (Univ.subst_univs_level_level subst u) acc) 
-    uctx.uctx_univ_algebraic Univ.LSet.empty 
-  in
-  let vars = 
-    Univ.LMap.fold
-      (fun u v acc ->
-	Univ.LMap.add (Univ.subst_univs_level_level subst u) 
-          (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 -> UGraph.add_universe u false g)
-				   (Univ.ContextSet.levels ctx') g in
-  let initial = declare uctx.uctx_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;
-	       uctx_universes = univs;
-	       uctx_initial_universes = initial } in
-    uctx', subst
+let fix_undefined_variables evd =
+  { evd with universes = UState.fix_undefined_variables evd.universes }
 
 let refresh_undefined_universes evd =
-  let uctx', subst = refresh_undefined_univ_variables evd.universes in
+  let uctx', subst = UState.refresh_undefined_univ_variables evd.universes in
   let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in
     evd', subst
 
-let normalize_evar_universe_context uctx = 
-  let rec fixpoint uctx = 
-    let ((vars',algs'), us') = 
-      Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables
-        uctx.uctx_univ_algebraic
-    in
-      if Univ.ContextSet.equal us' uctx.uctx_local then uctx
-      else
-	let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in
-	let uctx' = 
-	  { uctx_names = uctx.uctx_names;
-	    uctx_local = us'; 
-	    uctx_univ_variables = vars'; 
-	    uctx_univ_algebraic = algs';
-	    uctx_universes = universes;
-	    uctx_initial_universes = uctx.uctx_initial_universes }
-	in fixpoint uctx'
-  in fixpoint uctx
+let normalize_evar_universe_context = UState.normalize
 
 let nf_univ_variables evd = 
   let subst, uctx' = normalize_evar_universe_context_variables evd.universes in
@@ -1346,14 +924,12 @@ let nf_constraints =
       Profile.profile1 nfconstrkey nf_constraints
   else nf_constraints
 
-let universe_of_name evd s = 
-  UNameMap.find s (fst evd.universes.uctx_names)
+let universe_of_name evd s = UState.universe_of_name evd.universes s
 
 let add_universe_name evd s l =
-  let names' = add_uctx_names s l evd.universes.uctx_names in
-    {evd with universes = {evd.universes with uctx_names = names'}}
+  { evd with universes = UState.add_universe_name evd.universes s l }
 
-let universes evd = evd.universes.uctx_universes
+let universes evd = UState.ugraph evd.universes
 
 (* Conversion w.r.t. an evar map and its local universes. *)
 
@@ -1362,10 +938,10 @@ let conversion_gen env evd pb t u =
   | Reduction.CONV -> 
     Reduction.trans_conv_universes 
       full_transparent_state ~evars:(existential_opt_value evd) env 
-      evd.universes.uctx_universes t u
+      (UState.ugraph evd.universes) t u
   | Reduction.CUMUL -> Reduction.trans_conv_leq_universes
      full_transparent_state ~evars:(existential_opt_value evd) env 
-    evd.universes.uctx_universes t u
+      (UState.ugraph evd.universes) t u
 
 (* let conversion_gen_key = Profile.declare_profile "conversion_gen" *)
 (* let conversion_gen = Profile.profile5 conversion_gen_key conversion_gen *)
@@ -1377,8 +953,10 @@ let test_conversion env d pb t u =
   try conversion_gen env d pb t u; true
   with _ -> false
 
+exception UniversesDiffer = UState.UniversesDiffer
+
 let eq_constr_univs evd t u =
-  let b, c = Universes.eq_constr_univs_infer evd.universes.uctx_universes t u in
+  let b, c = Universes.eq_constr_univs_infer (UState.ugraph evd.universes) t u in
     if b then 
       try let evd' = add_universe_constraints evd c in evd', b
       with Univ.UniverseInconsistency _ | UniversesDiffer -> evd, false
@@ -1393,7 +971,7 @@ let e_eq_constr_univs evdref t u =
 
 let emit_side_effects eff evd =
   { evd with effects = Declareops.union_side_effects eff evd.effects;
-	     universes = emit_universe_side_effects eff evd.universes }
+	     universes = UState.emit_side_effects eff evd.universes }
 
 let drop_side_effects evd =
   { evd with effects = Declareops.no_seff; }
@@ -1760,11 +1338,11 @@ let pr_evar_universe_context ctx =
   if is_empty_evar_universe_context ctx then mt ()
   else
     (str"UNIVERSES:"++brk(0,1)++ 
-       h 0 (Univ.pr_universe_context_set prl ctx.uctx_local) ++ fnl () ++
+       h 0 (Univ.pr_universe_context_set prl (evar_universe_context_set Univ.UContext.empty ctx)) ++ fnl () ++
      str"ALGEBRAIC UNIVERSES:"++brk(0,1)++
-     h 0 (Univ.LSet.pr prl ctx.uctx_univ_algebraic) ++ fnl() ++
+     h 0 (Univ.LSet.pr prl (UState.variables ctx)) ++ fnl() ++
      str"UNDEFINED UNIVERSES:"++brk(0,1)++
-       h 0 (Universes.pr_universe_opt_subst ctx.uctx_univ_variables) ++ fnl())
+       h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl())
 
 let print_env_short env =
   let pr_body n = function