Imported Upstream version 8.9.0upstream/8.9.0upstream

33 files changed, 2467 insertions, 2015 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index bd47a04f..e109cbd0 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -13,132 +13,8 @@ open Util
 open Names
 open Constr
 open Context
-open Evd
-
-module API :
-sig
-module ESorts :
-sig
-type t
-val make : Sorts.t -> t
-val kind : Evd.evar_map -> t -> Sorts.t
-val unsafe_to_sorts : t -> Sorts.t
-end
-module EInstance :
-sig
-type t
-val make : Univ.Instance.t -> t
-val kind : Evd.evar_map -> t -> Univ.Instance.t
-val empty : t
-val is_empty : t -> bool
-val unsafe_to_instance : t -> Univ.Instance.t
-end
-type t
-val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term
-val kind_upto : Evd.evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term
-val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type
-val whd_evar : Evd.evar_map -> t -> t
-val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t
-val of_constr : Constr.t -> t
-val to_constr : evar_map -> t -> Constr.t
-val unsafe_to_constr : t -> Constr.t
-val unsafe_eq : (t, Constr.t) eq
-val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, t) Context.Named.Declaration.pt
-val unsafe_to_named_decl : (t, t) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt
-val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
-val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, t) Context.Rel.Declaration.pt
-val to_rel_decl : Evd.evar_map -> (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
-end =
-struct
-
-module ESorts =
-struct
-  type t = Sorts.t
-  let make s = s
-  let kind sigma = function
-  | Sorts.Type u -> Sorts.sort_of_univ (Evd.normalize_universe sigma u)
-  | s -> s
-  let unsafe_to_sorts s = s
-end
-
-module EInstance =
-struct
-  type t = Univ.Instance.t
-  let make i = i
-  let kind sigma i =
-    if Univ.Instance.is_empty i then i
-    else Evd.normalize_universe_instance sigma i
-  let empty = Univ.Instance.empty
-  let is_empty = Univ.Instance.is_empty
-  let unsafe_to_instance t = t
-end
 
-type t = Constr.t
-
-let safe_evar_value sigma ev =
-  try Some (Evd.existential_value sigma ev)
-  with NotInstantiatedEvar | Not_found -> None
-
-let rec whd_evar sigma c =
-  match Constr.kind c with
-  | Evar ev ->
-    begin match safe_evar_value sigma ev with
-    | Some c -> whd_evar sigma c
-    | None -> c
-    end
-  | App (f, args) when isEvar f ->
-    (** Enforce smart constructor invariant on applications *)
-    let ev = destEvar f in
-    begin match safe_evar_value sigma ev with
-    | None -> c
-    | Some f -> whd_evar sigma (mkApp (f, args))
-    end
-  | Cast (c0, k, t) when isEvar c0 ->
-    (** Enforce smart constructor invariant on casts. *)
-    let ev = destEvar c0 in
-    begin match safe_evar_value sigma ev with
-    | None -> c
-    | Some c -> whd_evar sigma (mkCast (c, k, t))
-    end
-  | _ -> c
-
-let kind sigma c = Constr.kind (whd_evar sigma c)
-let kind_upto = kind
-let kind_of_type sigma c = Term.kind_of_type (whd_evar sigma c)
-let of_kind = Constr.of_kind
-let of_constr c = c
-let unsafe_to_constr c = c
-let unsafe_eq = Refl
-
-let rec to_constr sigma c = match Constr.kind c with
-| Evar ev ->
-  begin match safe_evar_value sigma ev with
-  | Some c -> to_constr sigma c
-  | None -> Constr.map (fun c -> to_constr sigma c) c
-  end
-| Sort (Sorts.Type u) ->
-  let u' = Evd.normalize_universe sigma u in
-  if u' == u then c else mkSort (Sorts.sort_of_univ u')
-| Const (c', u) when not (Univ.Instance.is_empty u) ->
-  let u' = Evd.normalize_universe_instance sigma u in
-  if u' == u then c else mkConstU (c', u')
-| Ind (i, u) when not (Univ.Instance.is_empty u) ->
-  let u' = Evd.normalize_universe_instance sigma u in
-  if u' == u then c else mkIndU (i, u')
-| Construct (co, u) when not (Univ.Instance.is_empty u) ->
-  let u' = Evd.normalize_universe_instance sigma u in
-  if u' == u then c else mkConstructU (co, u')
-| _ -> Constr.map (fun c -> to_constr sigma c) c
-
-let of_named_decl d = d
-let unsafe_to_named_decl d = d
-let of_rel_decl d = d
-let unsafe_to_rel_decl d = d
-let to_rel_decl sigma d = Context.Rel.Declaration.map_constr (to_constr sigma) d
-
-end
-
-include API
+include Evd.MiniEConstr
 
 type types = t
 type constr = t
@@ -201,6 +77,14 @@ let isFix sigma c = match kind sigma c with Fix _ -> true | _ -> false
 let isCoFix sigma c = match kind sigma c with CoFix _ -> true | _ -> false
 let isCase sigma c = match kind sigma c with Case _ -> true | _ -> false
 let isProj sigma c = match kind sigma c with Proj _ -> true | _ -> false
+
+let rec isType sigma c = match kind sigma c with
+  | Sort s -> (match ESorts.kind sigma s with
+      | Sorts.Type _ -> true
+      | _ -> false )
+  | Cast (c,_,_) -> isType sigma c
+  | _ -> false
+
 let isVarId sigma id c =
   match kind sigma c with Var id' -> Id.equal id id' | _ -> false
 let isRelN sigma n c =
@@ -381,8 +265,7 @@ let decompose_prod_n_assum sigma n c =
   in
   prodec_rec Context.Rel.empty n c
 
-let existential_type sigma (evk, args) =
-  of_constr (existential_type sigma (evk, Array.map unsafe_to_constr args))
+let existential_type = Evd.existential_type
 
 let map sigma f c = match kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
@@ -410,7 +293,7 @@ let map sigma f c = match kind sigma c with
       else mkLetIn (na, b', t', k')
   | App (b,l) ->
       let b' = f b in
-      let l' = Array.smartmap f l in
+      let l' = Array.Smart.map f l in
       if b'==b && l'==l then c
       else mkApp (b', l')
   | Proj (p,t) ->
@@ -418,23 +301,23 @@ let map sigma f c = match kind sigma c with
       if t' == t then c
       else mkProj (p, t')
   | Evar (e,l) ->
-      let l' = Array.smartmap f l in
+      let l' = Array.Smart.map f l in
       if l'==l then c
       else mkEvar (e, l')
   | Case (ci,p,b,bl) ->
       let b' = f b in
       let p' = f p in
-      let bl' = Array.smartmap f bl in
+      let bl' = Array.Smart.map f bl in
       if b'==b && p'==p && bl'==bl then c
       else mkCase (ci, p', b', bl')
   | Fix (ln,(lna,tl,bl)) ->
-      let tl' = Array.smartmap f tl in
-      let bl' = Array.smartmap f bl in
+      let tl' = Array.Smart.map f tl in
+      let bl' = Array.Smart.map f bl in
       if tl'==tl && bl'==bl then c
       else mkFix (ln,(lna,tl',bl'))
   | CoFix(ln,(lna,tl,bl)) ->
-      let tl' = Array.smartmap f tl in
-      let bl' = Array.smartmap f bl in
+      let tl' = Array.Smart.map f tl in
+      let bl' = Array.Smart.map f bl in
       if tl'==tl && bl'==bl then c
       else mkCoFix (ln,(lna,tl',bl'))
 
@@ -464,7 +347,7 @@ let map_with_binders sigma g f l c0 = match kind sigma c0 with
     else mkLetIn (na, b', t', c')
   | App (c, al) ->
     let c' = f l c in
-    let al' = CArray.Fun1.smartmap f l al in
+    let al' = Array.Fun1.Smart.map f l al in
     if c' == c && al' == al then c0
     else mkApp (c', al')
   | Proj (p, t) ->
@@ -472,25 +355,25 @@ let map_with_binders sigma g f l c0 = match kind sigma c0 with
     if t' == t then c0
     else mkProj (p, t')
   | Evar (e, al) ->
-    let al' = CArray.Fun1.smartmap f l al in
+    let al' = Array.Fun1.Smart.map f l al in
     if al' == al then c0
     else mkEvar (e, al')
   | Case (ci, p, c, bl) ->
     let p' = f l p in
     let c' = f l c in
-    let bl' = CArray.Fun1.smartmap f l bl in
+    let bl' = Array.Fun1.Smart.map f l bl in
     if p' == p && c' == c && bl' == bl then c0
     else mkCase (ci, p', c', bl')
   | Fix (ln, (lna, tl, bl)) ->
-    let tl' = CArray.Fun1.smartmap f l tl in
+    let tl' = Array.Fun1.Smart.map f l tl in
     let l' = iterate g (Array.length tl) l in
-    let bl' = CArray.Fun1.smartmap f l' bl in
+    let bl' = Array.Fun1.Smart.map f l' bl in
     if tl' == tl && bl' == bl then c0
     else mkFix (ln,(lna,tl',bl'))
   | CoFix(ln,(lna,tl,bl)) ->
-    let tl' = CArray.Fun1.smartmap f l tl in
+    let tl' = Array.Fun1.Smart.map f l tl in
     let l' = iterate g (Array.length tl) l in
-    let bl' = CArray.Fun1.smartmap f l' bl in
+    let bl' = Array.Fun1.Smart.map f l' bl in
     mkCoFix (ln,(lna,tl',bl'))
 
 let iter sigma f c = match kind sigma c with
@@ -516,9 +399,9 @@ let iter_with_full_binders sigma g f n c =
   | Prod (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
   | Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
   | LetIn (na,b,t,c) -> f n b; f n t; f (g (LocalDef (na, b, t)) n) c
-  | App (c,l) -> f n c; CArray.Fun1.iter f n l
-  | Evar (_,l) -> CArray.Fun1.iter f n l
-  | Case (_,p,c,bl) -> f n p; f n c; CArray.Fun1.iter f n bl
+  | App (c,l) -> f n c; Array.Fun1.iter f n l
+  | Evar (_,l) -> Array.Fun1.iter f n l
+  | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl
   | Proj (p,c) -> f n c
   | Fix (_,(lna,tl,bl)) ->
     Array.iter (f n) tl;
@@ -551,10 +434,22 @@ let fold sigma f acc c = match kind sigma c with
 let compare_gen k eq_inst eq_sort eq_constr nargs c1 c2 =
   (c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr nargs c1 c2
 
+let eq_einstance sigma i1 i2 =
+  let i1 = EInstance.kind sigma (EInstance.make i1) in
+  let i2 = EInstance.kind sigma (EInstance.make i2) in
+  Univ.Instance.equal i1 i2
+
+let eq_esorts sigma s1 s2 =
+  let s1 = ESorts.kind sigma (ESorts.make s1) in
+  let s2 = ESorts.kind sigma (ESorts.make s2) in
+  Sorts.equal s1 s2
+
 let eq_constr sigma c1 c2 =
   let kind c = kind_upto sigma c in
+  let eq_inst _ _ i1 i2 = eq_einstance sigma i1 i2 in
+  let eq_sorts s1 s2 = eq_esorts sigma s1 s2 in
   let rec eq_constr nargs c1 c2 =
-    compare_gen kind (fun _ _ -> Univ.Instance.equal) Sorts.equal eq_constr nargs c1 c2
+    compare_gen kind eq_inst eq_sorts eq_constr nargs c1 c2
   in
   eq_constr 0 (unsafe_to_constr c1) (unsafe_to_constr c2)
 
@@ -567,32 +462,34 @@ let eq_constr_nounivs sigma c1 c2 =
 
 let compare_constr sigma cmp c1 c2 =
   let kind c = kind_upto sigma c in
+  let eq_inst _ _ i1 i2 = eq_einstance sigma i1 i2 in
+  let eq_sorts s1 s2 = eq_esorts sigma s1 s2 in
   let cmp nargs c1 c2 = cmp (of_constr c1) (of_constr c2) in
-  compare_gen kind (fun _ _ -> Univ.Instance.equal) Sorts.equal cmp 0 (unsafe_to_constr c1) (unsafe_to_constr c2)
+  compare_gen kind eq_inst eq_sorts cmp 0 (unsafe_to_constr c1) (unsafe_to_constr c2)
 
 let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs =
-  let open Universes in
+  let open UnivProblem in
   if not nargs_ok then enforce_eq_instances_univs false u u' cstrs
   else
     CArray.fold_left3
       (fun cstrs v u u' ->
          let open Univ.Variance in
          match v with
-         | Irrelevant -> Constraints.add (UWeak (u,u')) cstrs
+         | Irrelevant -> Set.add (UWeak (u,u')) cstrs
          | Covariant ->
            let u = Univ.Universe.make u in
            let u' = Univ.Universe.make u' in
            (match cv_pb with
-            | Reduction.CONV -> Constraints.add (UEq (u,u')) cstrs
-            | Reduction.CUMUL -> Constraints.add (ULe (u,u')) cstrs)
+            | Reduction.CONV -> Set.add (UEq (u,u')) cstrs
+            | Reduction.CUMUL -> Set.add (ULe (u,u')) cstrs)
          | Invariant ->
            let u = Univ.Universe.make u in
            let u' = Univ.Universe.make u' in
-           Constraints.add (UEq (u,u')) cstrs)
+           Set.add (UEq (u,u')) cstrs)
       cstrs variances (Univ.Instance.to_array u) (Univ.Instance.to_array u')
 
 let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs =
-  let open Universes in
+  let open UnivProblem in
   match mind.Declarations.mind_universes with
   | Declarations.Monomorphic_ind _ ->
     assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0);
@@ -605,7 +502,7 @@ let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs =
     compare_cumulative_instances cv_pb (Int.equal num_param_arity nargs) variances u1 u2 cstrs
 
 let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs =
-  let open Universes in
+  let open UnivProblem in
   match mind.Declarations.mind_universes with
   | Declarations.Monomorphic_ind _ ->
     cstrs
@@ -616,7 +513,7 @@ let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs =
     if not (Int.equal num_cnstr_args nargs)
     then enforce_eq_instances_univs false u1 u2 cstrs
     else
-      Array.fold_left2 (fun cstrs u1 u2 -> Universes.(Constraints.add (UWeak (u1,u2)) cstrs))
+      Array.fold_left2 (fun cstrs u1 u2 -> UnivProblem.(Set.add (UWeak (u1,u2)) cstrs))
         cstrs (Univ.Instance.to_array u1) (Univ.Instance.to_array u2)
 
 let eq_universes env sigma cstrs cv_pb ref nargs l l' =
@@ -624,7 +521,8 @@ let eq_universes env sigma cstrs cv_pb ref nargs l l' =
   else
     let l = Evd.normalize_universe_instance sigma l
     and l' = Evd.normalize_universe_instance sigma l' in
-    let open Universes in
+    let open GlobRef in
+    let open UnivProblem in
     match ref with
     | VarRef _ -> assert false (* variables don't have instances *)
     | ConstRef _ ->
@@ -639,11 +537,11 @@ let eq_universes env sigma cstrs cv_pb ref nargs l l' =
       true
 
 let test_constr_universes env sigma leq m n =
-  let open Universes in
+  let open UnivProblem in
   let kind c = kind_upto sigma c in
-  if m == n then Some Constraints.empty
+  if m == n then Some Set.empty
   else
-    let cstrs = ref Constraints.empty in
+    let cstrs = ref Set.empty in
     let cv_pb = if leq then Reduction.CUMUL else Reduction.CONV in
     let eq_universes ref nargs l l' = eq_universes env sigma cstrs Reduction.CONV ref nargs l l'
     and leq_universes ref nargs l l' = eq_universes env sigma cstrs cv_pb ref nargs l l' in
@@ -651,7 +549,7 @@ let test_constr_universes env sigma leq m n =
       let s1 = ESorts.kind sigma (ESorts.make s1) in
       let s2 = ESorts.kind sigma (ESorts.make s2) in
       if Sorts.equal s1 s2 then true
-      else (cstrs := Constraints.add 
+      else (cstrs := Set.add
               (UEq (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs;
 	    true)
     in
@@ -660,7 +558,7 @@ let test_constr_universes env sigma leq m n =
       let s2 = ESorts.kind sigma (ESorts.make s2) in
       if Sorts.equal s1 s2 then true
       else 
-	(cstrs := Constraints.add 
+        (cstrs := Set.add
            (ULe (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs;
 	 true)
     in
@@ -689,24 +587,23 @@ let compare_head_gen_proj env sigma equ eqs eqc' nargs m n =
   | App (f, args), Proj (p, c) -> 
       (match kind_upto sigma f with
       | Const (p', u) when Constant.equal (Projection.constant p) p' -> 
-          let pb = Environ.lookup_projection p env in
-          let npars = pb.Declarations.proj_npars in
-	  if Array.length args == npars + 1 then
+          let npars = Projection.npars p in
+          if Array.length args == npars + 1 then
             eqc' 0 c args.(npars)
 	  else false
       | _ -> false)
   | _ -> Constr.compare_head_gen_with kind kind equ eqs eqc' nargs m n
 
 let eq_constr_universes_proj env sigma m n =
-  let open Universes in
-  if m == n then Some Constraints.empty
+  let open UnivProblem in
+  if m == n then Some Set.empty
   else 
-    let cstrs = ref Constraints.empty in
+    let cstrs = ref Set.empty in
     let eq_universes ref l l' = eq_universes env sigma cstrs Reduction.CONV ref l l' in
     let eq_sorts s1 s2 =
       if Sorts.equal s1 s2 then true
       else
-	(cstrs := Constraints.add 
+        (cstrs := Set.add
            (UEq (Sorts.univ_of_sort s1, Sorts.univ_of_sort s2)) !cstrs;
 	 true)
     in
@@ -716,25 +613,14 @@ let eq_constr_universes_proj env sigma m n =
     let res = eq_constr' 0 (unsafe_to_constr m) (unsafe_to_constr n) in
     if res then Some !cstrs else None
 
-let universes_of_constr env sigma c =
+let universes_of_constr sigma c =
   let open Univ in
-  let open Declarations in
   let rec aux s c =
     match kind sigma c with
     | Const (c, u) ->
-      begin match (Environ.lookup_constant c env).const_universes with
-        | Polymorphic_const _ ->
           LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
-        | Monomorphic_const (univs, _) ->
-          LSet.union s univs
-      end
     | Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
-      begin match (Environ.lookup_mind mind env).mind_universes with
-        | Cumulative_ind _ | Polymorphic_ind _ ->
           LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
-        | Monomorphic_ind (univs,_) ->
-          LSet.union s univs
-      end
     | Sort u ->
        let sort = ESorts.kind sigma u in
        if Sorts.is_small sort then s
@@ -743,7 +629,7 @@ let universes_of_constr env sigma c =
          LSet.fold LSet.add (Universe.levels u) s
     | Evar (k, args) ->
        let concl = Evd.evar_concl (Evd.find sigma k) in
-       fold sigma aux (aux s (of_constr concl)) c
+       fold sigma aux (aux s concl) c
     | _ -> fold sigma aux s c
   in aux LSet.empty c
 
@@ -901,9 +787,13 @@ let named_context e = cast_named_context (sym unsafe_eq) (named_context e)
 let val_of_named_context e = val_of_named_context (cast_named_context unsafe_eq e)
 let named_context_of_val e = cast_named_context (sym unsafe_eq) (named_context_of_val e)
 
+let of_existential : Constr.existential -> existential =
+  let gen : type a b. (a,b) eq -> 'c * b array -> 'c * a array = fun Refl x -> x in
+  gen unsafe_eq
+
 let lookup_rel i e = cast_rel_decl (sym unsafe_eq) (lookup_rel i e)
 let lookup_named n e = cast_named_decl (sym unsafe_eq) (lookup_named n e)
-let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_val n e)
+let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_ctxt n e)
 
 let map_rel_context_in_env f env sign =
   let rec aux env acc = function
@@ -916,7 +806,7 @@ let map_rel_context_in_env f env sign =
 
 let fresh_global ?loc ?rigid ?names env sigma reference =
   let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in
-  evd, of_constr t
+  evd, t
 
 let is_global sigma gr c =
   Globnames.is_global gr (to_constr sigma c)
@@ -928,5 +818,10 @@ let to_instance = EInstance.unsafe_to_instance
 let to_constr = unsafe_to_constr
 let to_rel_decl = unsafe_to_rel_decl
 let to_named_decl = unsafe_to_named_decl
+let to_named_context =
+  let gen : type a b. (a, b) eq -> (a,a) Context.Named.pt -> (b,b) Context.Named.pt
+    = fun Refl x -> x
+  in
+  gen unsafe_eq
 let eq = unsafe_eq
 end
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 8ee3b905..00c6d7ce 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -13,7 +13,7 @@ open Names
 open Constr
 open Environ
 
-type t
+type t = Evd.econstr
 (** Type of incomplete terms. Essentially a wrapper around {!Constr.t} ensuring
     that {!Constr.kind} does not observe defined evars. *)
 
@@ -68,11 +68,14 @@ val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_ter
 
 val kind_upto : Evd.evar_map -> Constr.t -> (Constr.t, Constr.t, Sorts.t, Univ.Instance.t) Constr.kind_of_term
 
-val to_constr : Evd.evar_map -> t -> Constr.t
-(** Returns the evar-normal form of the argument, and cast it as a theoretically
-    evar-free term. In practice this function does not check that the result
-    is actually evar-free, it is currently the duty of the caller to do so.
-    This might change in the future. *)
+val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t
+(** Returns the evar-normal form of the argument. Note that this
+   function is supposed to be called when the original term has not
+   more free-evars anymore. If you need compatibility with the old
+   semantics, set [abort_on_undefined_evars] to [false].
+
+    For getting the evar-normal form of a term with evars see
+   {!Evarutil.nf_evar}. *)
 
 val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type
 
@@ -152,6 +155,8 @@ val isCoFix : Evd.evar_map -> t -> bool
 val isCase : Evd.evar_map -> t -> bool
 val isProj : Evd.evar_map -> t -> bool
 
+val isType : Evd.evar_map -> constr -> bool
+
 type arity = rel_context * ESorts.t
 val destArity : Evd.evar_map -> types -> arity
 val isArity : Evd.evar_map -> t -> bool
@@ -179,9 +184,21 @@ val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint
 
 val decompose_app : Evd.evar_map -> t -> t * t list
 
+(** Pops lambda abstractions until there are no more, skipping casts. *)
 val decompose_lam : Evd.evar_map -> t -> (Name.t * t) list * t
+
+(** Pops lambda abstractions and letins until there are no more, skipping casts. *)
 val decompose_lam_assum : Evd.evar_map -> t -> rel_context * t
+
+(** Pops [n] lambda abstractions, and pop letins only if needed to
+   expose enough lambdas, skipping casts.
+
+    @raise UserError if the term doesn't have enough lambdas. *)
 val decompose_lam_n_assum : Evd.evar_map -> int -> t -> rel_context * t
+
+(** Pops [n] lambda abstractions and letins, skipping casts.
+
+     @raise UserError if the term doesn't have enough lambdas/letins. *)
 val decompose_lam_n_decls : Evd.evar_map -> int -> t -> rel_context * t
 
 val compose_lam : (Name.t * t) list -> t -> t
@@ -198,11 +215,11 @@ val whd_evar : Evd.evar_map -> constr -> constr
 
 val eq_constr : Evd.evar_map -> t -> t -> bool
 val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool
-val eq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option
-val leq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option
+val eq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> UnivProblem.Set.t option
+val leq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> UnivProblem.Set.t option
 
 (** [eq_constr_universes_proj] can equate projections and their eta-expanded constant form. *)
-val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option
+val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> UnivProblem.Set.t option
 
 val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool
 
@@ -217,7 +234,7 @@ val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a
 
 (** Gather the universes transitively used in the term, including in the
    type of evars appearing in it. *)
-val universes_of_constr : Environ.env -> Evd.evar_map -> t -> Univ.LSet.t
+val universes_of_constr : Evd.evar_map -> t -> Univ.LSet.t
 
 (** {6 Substitutions} *)
 
@@ -281,12 +298,13 @@ val map_rel_context_in_env :
 (* XXX Missing Sigma proxy *)
 val fresh_global :
   ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
-  Evd.evar_map -> Globnames.global_reference -> Evd.evar_map * t
+  Evd.evar_map -> GlobRef.t -> Evd.evar_map * t
 
-val is_global : Evd.evar_map -> Globnames.global_reference -> t -> bool
+val is_global : Evd.evar_map -> GlobRef.t -> t -> bool
 
 (** {5 Extra} *)
 
+val of_existential : Constr.existential -> existential
 val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, types) Context.Named.Declaration.pt
 val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, types) Context.Rel.Declaration.pt
 
@@ -305,6 +323,8 @@ sig
   val to_named_decl : (t, types) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt
   (** Physical identity. Does not care for defined evars. *)
 
+  val to_named_context : (t, types) Context.Named.pt -> Constr.named_context
+
   val to_sorts : ESorts.t -> Sorts.t
   (** Physical identity. Does not care for normalization. *)
 
diff --git a/engine/engine.mllib b/engine/engine.mllib
index a3614f6c..37e83b62 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -1,7 +1,13 @@
+UnivNames
+UnivGen
+UnivSubst
+UnivProblem
+UnivMinim
 Universes
 Univops
 UState
 Nameops
+Evar_kinds
 Evd
 EConstr
 Namegen
diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml
new file mode 100644
index 00000000..ea1e5725
--- /dev/null
+++ b/engine/evar_kinds.ml
@@ -0,0 +1,52 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+
+(** The kinds of existential variable *)
+
+(** Should the obligation be defined (opaque or transparent (default)) or
+    defined transparent and expanded in the term? *)
+
+type obligation_definition_status = Define of bool | Expand
+
+type matching_var_kind = FirstOrderPatVar of Id.t | SecondOrderPatVar of Id.t
+
+type subevar_kind = Domain | Codomain | Body
+
+(* maybe this should be a Projection.t *)
+type record_field = { fieldname : Constant.t; recordname : Names.inductive }
+
+type question_mark = {
+     qm_obligation: obligation_definition_status;
+     qm_name: Name.t;
+     qm_record_field: record_field option;
+}
+
+let default_question_mark = {
+  qm_obligation=Define true;
+  qm_name=Anonymous;
+  qm_record_field=None;
+}
+
+type t =
+  | ImplicitArg of GlobRef.t * (int * Id.t option)
+     * bool (** Force inference *)
+  | BinderType of Name.t
+  | NamedHole of Id.t (* coming from some ?[id] syntax *)
+  | QuestionMark of question_mark
+  | CasesType of bool (* true = a subterm of the type *)
+  | InternalHole
+  | TomatchTypeParameter of inductive * int
+  | GoalEvar
+  | ImpossibleCase
+  | MatchingVar of matching_var_kind
+  | VarInstance of Id.t
+  | SubEvar of subevar_kind option * Evar.t
diff --git a/engine/evar_kinds.mli b/engine/evar_kinds.mli
new file mode 100644
index 00000000..4facdb20
--- /dev/null
+++ b/engine/evar_kinds.mli
@@ -0,0 +1,51 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+
+(** The kinds of existential variable *)
+
+(** Should the obligation be defined (opaque or transparent (default)) or
+    defined transparent and expanded in the term? *)
+
+type obligation_definition_status = Define of bool | Expand
+
+type matching_var_kind = FirstOrderPatVar of Id.t | SecondOrderPatVar of Id.t
+
+type subevar_kind = Domain | Codomain | Body
+
+(* maybe this should be a Projection.t *)
+(* Represents missing record field *)
+type record_field = { fieldname : Constant.t; recordname : Names.inductive }
+
+type question_mark = {
+     qm_obligation: obligation_definition_status;
+     qm_name: Name.t;
+     (* Tracks if the evar represents a missing record field *)
+     qm_record_field: record_field option;
+}
+
+(* Default value of question_mark which is used most often *)
+val default_question_mark : question_mark
+
+type t =
+  | ImplicitArg of GlobRef.t * (int * Id.t option)
+     * bool (** Force inference *)
+  | BinderType of Name.t
+  | NamedHole of Id.t (* coming from some ?[id] syntax *)
+  | QuestionMark of question_mark
+  | CasesType of bool (* true = a subterm of the type *)
+  | InternalHole
+  | TomatchTypeParameter of inductive * int
+  | GoalEvar
+  | ImpossibleCase
+  | MatchingVar of matching_var_kind
+  | VarInstance of Id.t
+  | SubEvar of subevar_kind option * Evar.t
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 9cf81ecc..b77bf55d 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -13,7 +13,6 @@ open Util
 open Names
 open Term
 open Constr
-open Pre_env
 open Environ
 open Evd
 open Termops
@@ -23,7 +22,8 @@ module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
 let safe_evar_value sigma ev =
-  try Some (Evd.existential_value sigma ev)
+  let ev = EConstr.of_existential ev in
+  try Some (EConstr.Unsafe.to_constr @@ Evd.existential_value sigma ev)
   with NotInstantiatedEvar | Not_found -> None
 
 (** Combinators *)
@@ -44,11 +44,11 @@ let evd_comb2 f evdref x y =
     z
 
 let e_new_global evdref x = 
-  EConstr.of_constr (evd_comb1 (Evd.fresh_global (Global.env())) evdref x)
+  evd_comb1 (Evd.fresh_global (Global.env())) evdref x
 
 let new_global evd x = 
   let (evd, c) = Evd.fresh_global (Global.env()) evd x in
-  (evd, EConstr.of_constr c)
+  (evd, c)
 
 (****************************************************)
 (* Expanding/testing/exposing existential variables *)
@@ -61,7 +61,7 @@ exception Uninstantiated_evar of Evar.t
 let rec flush_and_check_evars sigma c =
   match kind c with
   | Evar (evk,_ as ev) ->
-      (match existential_opt_value sigma ev with
+      (match existential_opt_value0 sigma ev with
        | None -> raise (Uninstantiated_evar evk)
        | Some c -> flush_and_check_evars sigma c)
   | _ -> Constr.map (flush_and_check_evars sigma) c
@@ -72,9 +72,9 @@ let flush_and_check_evars sigma c =
 (** Term exploration up to instantiation. *)
 let kind_of_term_upto = EConstr.kind_upto
 
-let nf_evar0 sigma t = EConstr.to_constr sigma (EConstr.of_constr t)
+let nf_evar0 sigma t = EConstr.to_constr ~abort_on_undefined_evars:false sigma (EConstr.of_constr t)
 let whd_evar = EConstr.whd_evar
-let nf_evar sigma c = EConstr.of_constr (EConstr.to_constr sigma c)
+let nf_evar sigma c = EConstr.of_constr (EConstr.to_constr ~abort_on_undefined_evars:false sigma c)
 
 let j_nf_evar sigma j =
   { uj_val = nf_evar sigma j.uj_val;
@@ -85,7 +85,7 @@ let tj_nf_evar sigma {utj_val=v;utj_type=t} =
   {utj_val=nf_evar sigma v;utj_type=t}
 
 let nf_evars_universes evm =
-  Universes.nf_evars_and_universes_opt_subst (safe_evar_value evm) 
+  UnivSubst.nf_evars_and_universes_opt_subst (safe_evar_value evm)
     (Evd.universe_subst evm)
     
 let nf_evars_and_universes evm =
@@ -102,7 +102,8 @@ let nf_evar_map_universes evm =
     if Univ.LMap.is_empty subst then evm, nf_evar0 evm
     else
       let f = nf_evars_universes evm in
-	Evd.raw_map (fun _ -> map_evar_info f) evm, f
+      let f' c = EConstr.of_constr (f (EConstr.Unsafe.to_constr c)) in
+        Evd.raw_map (fun _ -> map_evar_info f') evm, f
 
 let nf_named_context_evar sigma ctx =
   Context.Named.map (nf_evar0 sigma) ctx
@@ -115,7 +116,7 @@ let nf_env_evar sigma env =
   let rel' = nf_rel_context_evar sigma (EConstr.rel_context env) in
     EConstr.push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env)
 
-let nf_evar_info evc info = map_evar_info (nf_evar0 evc) info
+let nf_evar_info evc info = map_evar_info (nf_evar evc) info
 
 let nf_evar_map evm =
   Evd.raw_map (fun _ evi -> nf_evar_info evm evi) evm
@@ -212,7 +213,7 @@ let mk_new_meta () = EConstr.mkMeta(new_meta())
 
 let non_instantiated sigma =
   let listev = Evd.undefined_map sigma in
-  Evar.Map.smartmap (fun evi -> nf_evar_info sigma evi) listev
+  Evar.Map.Smart.map (fun evi -> nf_evar_info sigma evi) listev
 
 (************************)
 (* Manipulating filters *)
@@ -340,7 +341,15 @@ let update_var src tgt subst =
       let csubst_var = Id.Map.add id (Constr.mkVar tgt) subst.csubst_var in
       { subst with csubst_var; csubst_rev }
 
-let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) =
+type naming_mode =
+  | KeepUserNameAndRenameExistingButSectionNames
+  | KeepUserNameAndRenameExistingEvenSectionNames
+  | KeepExistingNames
+  | FailIfConflict
+
+let push_rel_decl_to_named_context
+  ?(hypnaming=KeepUserNameAndRenameExistingButSectionNames)
+  sigma decl (subst, avoid, nc) =
   let open EConstr in
   let open Vars in
   let map_decl f d =
@@ -371,7 +380,9 @@ let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) =
       next_ident_away (id_of_name_using_hdchar empty_env sigma (RelDecl.get_type decl) na) avoid
   in
   match extract_if_neq id na with
-  | Some id0 when not (is_section_variable id0) ->
+  | Some id0 when hypnaming = KeepUserNameAndRenameExistingEvenSectionNames ||
+                  hypnaming = KeepUserNameAndRenameExistingButSectionNames &&
+                  not (is_section_variable id0) ->
       (* spiwack: if [id<>id0], rather than introducing a new
           binding named [id], we will keep [id0] (the name given
           by the user) and rename [id0] into [id] in the named
@@ -380,6 +391,8 @@ let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) =
       let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (csubst_subst subst) in
       let nc = List.map (replace_var_named_declaration id0 id) nc in
       (push_var id0 subst, Id.Set.add id avoid, d :: nc)
+  | Some id0 when hypnaming = FailIfConflict ->
+       user_err Pp.(Id.print id0 ++ str " is already used.")
   | _ ->
       (* spiwack: if [id0] is a section variable renaming it is
           incorrect. We revert to a less robust behaviour where
@@ -388,7 +401,7 @@ let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) =
       let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (csubst_subst subst) in
       (push_var id subst, Id.Set.add id avoid, d :: nc)
 
-let push_rel_context_to_named_context env sigma typ =
+let push_rel_context_to_named_context ?hypnaming env sigma typ =
   (* compute the instances relative to the named context and rel_context *)
   let open Context.Named.Declaration in
   let open EConstr in
@@ -403,7 +416,7 @@ let push_rel_context_to_named_context env sigma typ =
     (* with vars of the rel context *)
     (* We do keep the instances corresponding to local definition (see above) *)
     let (subst, _, env) =
-      Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc)
+      Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context ?hypnaming sigma d acc)
         (rel_context env) ~init:(empty_csubst, avoid, named_context env) in
     (val_of_named_context env, csubst_subst subst typ, inst_rels@inst_vars, subst)
 
@@ -413,25 +426,18 @@ let push_rel_context_to_named_context env sigma typ =
 
 let default_source = Loc.tag @@ Evar_kinds.InternalHole
 
-let restrict_evar evd evk filter ?src candidates =
-  let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in
-  let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in
-  Evd.declare_future_goal evk' evd, evk'
-
 let new_pure_evar_full evd evi =
   let (evd, evk) = Evd.new_evar evd evi in
   let evd = Evd.declare_future_goal evk evd in
   (evd, evk)
 
-let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ =
-  let typ = EConstr.Unsafe.to_constr typ in
-  let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in
-  let default_naming = Misctypes.IntroAnonymous in
+let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) sign evd typ =
+  let default_naming = IntroAnonymous in
   let naming = Option.default default_naming naming in
   let name = match naming with
-  | Misctypes.IntroAnonymous -> None
-  | Misctypes.IntroIdentifier id -> Some id
-  | Misctypes.IntroFresh id ->
+  | IntroAnonymous -> None
+  | IntroIdentifier id -> Some id
+  | IntroFresh id ->
     let has_name id = try let _ = Evd.evar_key id evd in true with Not_found -> false in
     let id = Namegen.next_ident_away_from id has_name in
     Some id
@@ -452,14 +458,14 @@ let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?ca
   in
   (evd, newevk)
 
-let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance =
+let new_evar_instance ?src ?filter ?candidates ?store ?naming ?principal sign evd typ instance =
   let open EConstr in
   assert (not !Flags.debug ||
             List.distinct (ids_of_named_context (named_context_of_val sign)));
   let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
   evd, mkEvar (newevk,Array.of_list instance)
 
-let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?principal typ =
+let new_evar_from_context ?src ?filter ?candidates ?store ?naming ?principal sign evd typ =
   let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
   let instance =
     match filter with
@@ -469,8 +475,8 @@ let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?prin
 
 (* [new_evar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
-let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
-  let sign,typ',instance,subst = push_rel_context_to_named_context env evd typ in
+let new_evar ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming env evd typ =
+  let sign,typ',instance,subst = push_rel_context_to_named_context ?hypnaming env evd typ in
   let map c = csubst_subst subst c in
   let candidates = Option.map (fun l -> List.map map l) candidates in
   let instance =
@@ -479,31 +485,46 @@ let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
     | Some filter -> Filter.filter_list filter instance in
   new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance
 
-let new_type_evar env evd ?src ?filter ?naming ?principal rigid =
+let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid =
   let (evd', s) = new_sort_variable rigid evd in
-  let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal (EConstr.mkSort s) in
+  let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal ?hypnaming (EConstr.mkSort s) in
   evd', (e, s)
 
-let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid =
-  let (evd, c) = new_type_evar env !evdref ?src ?filter ?naming ?principal rigid in
+let e_new_type_evar env evdref ?src ?filter ?naming ?principal ?hypnaming rigid =
+  let (evd, c) = new_type_evar env !evdref ?src ?filter ?naming ?principal ?hypnaming rigid in
     evdref := evd;
     c
 
-let new_Type ?(rigid=Evd.univ_flexible) env evd = 
+let new_Type ?(rigid=Evd.univ_flexible) evd =
   let open EConstr in
   let (evd, s) = new_sort_variable rigid evd in
   (evd, mkSort s)
 
-let e_new_Type ?(rigid=Evd.univ_flexible) env evdref =
+let e_new_Type ?(rigid=Evd.univ_flexible) evdref =
   let evd', s = new_sort_variable rigid !evdref in
     evdref := evd'; EConstr.mkSort s
 
   (* The same using side-effect *)
-let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ty =
-  let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ty in
+let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ?hypnaming ty =
+  let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ?hypnaming ty in
   evdref := evd';
   ev
 
+(* Safe interface to unification problems *)
+type unification_pb = conv_pb * env * EConstr.constr * EConstr.constr
+
+let eq_unification_pb evd (pbty,env,t1,t2) (pbty',env',t1',t2') =
+  pbty == pbty' && env == env' &&
+    EConstr.eq_constr evd t1 t1' &&
+    EConstr.eq_constr evd t2 t2'
+
+let add_unification_pb ?(tail=false) pb evd =
+  let conv_pbs = Evd.conv_pbs evd in
+  if not (List.exists (eq_unification_pb evd pb) conv_pbs) then
+    let (pbty,env,t1,t2) = pb in
+    Evd.add_conv_pb ~tail (pbty,env,t1,t2) evd
+  else evd
+
 (* This assumes an evar with identity instance and generalizes it over only
    the de Bruijn part of the context *)
 let generalize_evar_over_rels sigma (ev,args) =
@@ -513,7 +534,7 @@ let generalize_evar_over_rels sigma (ev,args) =
   List.fold_left2
     (fun (c,inst as x) a d ->
       if isRel sigma a then (mkNamedProd_or_LetIn d c,a::inst) else x)
-     (EConstr.of_constr evi.evar_concl,[]) (Array.to_list args) sign
+     (evi.evar_concl,[]) (Array.to_list args) sign
 
 (************************************)
 (* Removing a dependency in an evar *)
@@ -522,11 +543,33 @@ let generalize_evar_over_rels sigma (ev,args) =
 type clear_dependency_error =
 | OccurHypInSimpleClause of Id.t option
 | EvarTypingBreak of existential
+| NoCandidatesLeft of Evar.t
 
-exception ClearDependencyError of Id.t * clear_dependency_error
+exception ClearDependencyError of Id.t * clear_dependency_error * GlobRef.t option
 
 exception Depends of Id.t
 
+let set_of_evctx l =
+  List.fold_left (fun s decl -> Id.Set.add (NamedDecl.get_id decl) s) Id.Set.empty l
+
+let filter_effective_candidates evd evi filter candidates =
+  let ids = set_of_evctx (Filter.filter_list filter (evar_context evi)) in
+  List.filter (fun a -> Id.Set.subset (collect_vars evd a) ids) candidates
+
+let restrict_evar evd evk filter ?src candidates =
+  let evar_info = Evd.find_undefined evd evk in
+  let candidates = Option.map (filter_effective_candidates evd evar_info filter) candidates in
+  match candidates with
+  | Some [] -> raise (ClearDependencyError (*FIXME*)(Id.of_string "blah", (NoCandidatesLeft evk), None))
+  | _ ->
+     let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in
+     (** Mark new evar as future goal, removing previous one,
+         circumventing Proofview.advance but making Proof.run_tactic catch these. *)
+     let future_goals = Evd.save_future_goals evd in
+     let future_goals = Evd.filter_future_goals (fun evk' -> not (Evar.equal evk evk')) future_goals in
+     let evd = Evd.restore_future_goals evd future_goals in
+     (Evd.declare_future_goal evk' evd, evk')
+
 let rec check_and_clear_in_constr env evdref err ids global c =
   (* returns a new constr where all the evars have been 'cleaned'
      (ie the hypotheses ids have been removed from the contexts of
@@ -534,13 +577,13 @@ let rec check_and_clear_in_constr env evdref err ids global c =
      is a section variable *)
     match kind c with
       | Var id' ->
-      if Id.Set.mem id' ids then raise (ClearDependencyError (id', err)) else c
+      if Id.Set.mem id' ids then raise (ClearDependencyError (id', err, None)) else c
 
       | ( Const _ | Ind _ | Construct _ ) ->
         let () = if global then
           let check id' =
             if Id.Set.mem id' ids then
-              raise (ClearDependencyError (id',err))
+              raise (ClearDependencyError (id',err,Some (Globnames.global_of_constr c)))
           in
           Id.Set.iter check (Environ.vars_of_global env c)
         in
@@ -549,7 +592,8 @@ let rec check_and_clear_in_constr env evdref err ids global c =
       | Evar (evk,l as ev) ->
 	  if Evd.is_defined !evdref evk then
 	    (* If evk is already defined we replace it by its definition *)
-	    let nc = Evd.existential_value !evdref ev in
+            let nc = Evd.existential_value !evdref (EConstr.of_existential ev) in
+            let nc = EConstr.Unsafe.to_constr nc in
 	      (check_and_clear_in_constr env evdref err ids global nc)
 	  else
 	    (* We check for dependencies to elements of ids in the
@@ -559,8 +603,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
 	       removed *)
 	    let evi = Evd.find_undefined !evdref evk in
 	    let ctxt = Evd.evar_filtered_context evi in
-	    let ctxt = List.map (fun d -> map_named_decl EConstr.of_constr d) ctxt in
-	    let (rids,filter) =
+            let (rids,filter) =
               List.fold_right2
                 (fun h a (ri,filter) ->
                   try
@@ -586,25 +629,29 @@ let rec check_and_clear_in_constr env evdref err ids global c =
 	      try
                 let nids = Id.Map.domain rids in
                 let global = Id.Set.exists is_section_variable nids in
-                check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids global (evar_concl evi)
-	      with ClearDependencyError (rid,err) ->
-		raise (ClearDependencyError (Id.Map.find rid rids,err)) in
+                let concl = EConstr.Unsafe.to_constr (evar_concl evi) in
+                check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids global concl
+              with ClearDependencyError (rid,err,where) ->
+                raise (ClearDependencyError (Id.Map.find rid rids,err,where)) in
 
             if Id.Map.is_empty rids then c
             else
               let origfilter = Evd.evar_filter evi in
               let filter = Evd.Filter.apply_subfilter origfilter filter in
               let evd = !evdref in
-              let (evd,_) = restrict_evar evd evk filter None in
+              let candidates = Evd.evar_candidates evi in
+              let candidates = Option.map (List.map EConstr.of_constr) candidates in
+              let (evd,_) = restrict_evar evd evk filter candidates in
               evdref := evd;
-              Evd.existential_value !evdref ev
+              Evd.existential_value0 !evdref ev
 
       | _ -> Constr.map (check_and_clear_in_constr env evdref err ids global) c
 
-let clear_hyps_in_evi_main env evdref hyps terms ids =
+let clear_hyps_in_evi_main env sigma hyps terms ids =
   (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
      hypothesis does not depend on a element of ids, and erases ids in
      the contexts of the evars occurring in evi *)
+  let evdref = ref sigma in
   let terms = List.map EConstr.Unsafe.to_constr terms in
   let global = Id.Set.exists is_section_variable ids in
   let terms =
@@ -627,23 +674,23 @@ let clear_hyps_in_evi_main env evdref hyps terms ids =
     in
       remove_hyps ids check_context check_value hyps
   in
-  (nhyps,List.map EConstr.of_constr terms)
+  (!evdref, nhyps,List.map EConstr.of_constr terms)
 
-let clear_hyps_in_evi env evdref hyps concl ids =
-  match clear_hyps_in_evi_main env evdref hyps [concl] ids with
-  | (nhyps,[nconcl]) -> (nhyps,nconcl)
+let clear_hyps_in_evi env sigma hyps concl ids =
+  match clear_hyps_in_evi_main env sigma hyps [concl] ids with
+  | (sigma,nhyps,[nconcl]) -> (sigma,nhyps,nconcl)
   | _ -> assert false
 
-let clear_hyps2_in_evi env evdref hyps t concl ids =
-  match clear_hyps_in_evi_main env evdref hyps [t;concl] ids with
-  | (nhyps,[t;nconcl]) -> (nhyps,t,nconcl)
+let clear_hyps2_in_evi env sigma hyps t concl ids =
+  match clear_hyps_in_evi_main env sigma hyps [t;concl] ids with
+  | (sigma,nhyps,[t;nconcl]) -> (sigma,nhyps,t,nconcl)
   | _ -> assert false
 
 (* spiwack: a few functions to gather evars on which goals depend. *)
 let queue_set q is_dependent set =
   Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set
 let queue_term q is_dependent c =
-  queue_set q is_dependent (evars_of_term c)
+  queue_set q is_dependent (evars_of_term (EConstr.Unsafe.to_constr c))
 
 let process_dependent_evar q acc evm is_dependent e =
   let evi = Evd.find evm e in
@@ -656,12 +703,12 @@ let process_dependent_evar q acc evm is_dependent e =
     match decl with
     | LocalAssum _ -> ()
     | LocalDef (_,b,_) -> queue_term q true b
-  end (Environ.named_context_of_val evi.evar_hyps);
+  end (EConstr.named_context_of_val evi.evar_hyps);
   match evi.evar_body with
   | Evar_empty ->
       if is_dependent then Evar.Map.add e None acc else acc
   | Evar_defined b ->
-      let subevars = evars_of_term b in
+      let subevars = evars_of_term (EConstr.Unsafe.to_constr b) in
       (* evars appearing in the definition of an evar [e] are marked
          as dependent when [e] is dependent itself: if [e] is a
          non-dependent goal, then, unless they are reach from another
@@ -729,11 +776,11 @@ let undefined_evars_of_named_context evd nc =
     ~init:Evar.Set.empty
 
 let undefined_evars_of_evar_info evd evi =
-  Evar.Set.union (undefined_evars_of_term evd (EConstr.of_constr evi.evar_concl))
+  Evar.Set.union (undefined_evars_of_term evd evi.evar_concl)
     (Evar.Set.union
        (match evi.evar_body with
 	 | Evar_empty -> Evar.Set.empty
-	 | Evar_defined b -> undefined_evars_of_term evd (EConstr.of_constr b))
+         | Evar_defined b -> undefined_evars_of_term evd b)
        (undefined_evars_of_named_context evd
 	  (named_context_of_val evi.evar_hyps)))
 
@@ -781,10 +828,11 @@ let filtered_undefined_evars_of_evar_info ?cache sigma evi =
   in
   let accu = match evi.evar_body with
   | Evar_empty -> Evar.Set.empty
-  | Evar_defined b -> evars_of_term b
+  | Evar_defined b -> evars_of_term (EConstr.Unsafe.to_constr b)
   in
-  let accu = Evar.Set.union (undefined_evars_of_term sigma (EConstr.of_constr evi.evar_concl)) accu in
-  evars_of_named_context cache accu (evar_filtered_context evi)
+  let accu = Evar.Set.union (undefined_evars_of_term sigma evi.evar_concl) accu in
+  let ctxt = EConstr.Unsafe.to_named_context (evar_filtered_context evi) in
+  evars_of_named_context cache accu ctxt
 
 (* spiwack: this is a more complete version of
    {!Termops.occur_evar}. The latter does not look recursively into an
@@ -794,7 +842,7 @@ let occur_evar_upto sigma n c =
   let c = EConstr.Unsafe.to_constr c in
   let rec occur_rec c = match kind c with
     | Evar (sp,_) when Evar.equal sp n -> raise Occur
-    | Evar e -> Option.iter occur_rec (existential_opt_value sigma e)
+    | Evar e -> Option.iter occur_rec (existential_opt_value0 sigma e)
     | _ -> Constr.iter occur_rec c
   in
   try occur_rec c; false with Occur -> true
@@ -807,22 +855,22 @@ let judge_of_new_Type evd =
   let (evd', s) = new_univ_variable univ_rigid evd in
   (evd', { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) })
 
-let subterm_source evk (loc,k) =
+let subterm_source evk ?where (loc,k) =
   let evk = match k with
-    | Evar_kinds.SubEvar (evk) -> evk
+    | Evar_kinds.SubEvar (None,evk) when where = None -> evk
     | _ -> evk in
-  (loc,Evar_kinds.SubEvar evk)
+  (loc,Evar_kinds.SubEvar (where,evk))
 
 (* Add equality constraints for covariant/invariant positions. For
    irrelevant positions, unify universes when flexible. *)
 let compare_cumulative_instances cv_pb variances u u' sigma =
-  let open Universes in
+  let open UnivProblem in
   let cstrs = Univ.Constraint.empty in
-  let soft = Constraints.empty in
+  let soft = Set.empty in
   let cstrs, soft = Array.fold_left3 (fun (cstrs, soft) v u u' ->
       let open Univ.Variance in
       match v with
-      | Irrelevant -> cstrs, Constraints.add (UWeak (u,u')) soft
+      | Irrelevant -> cstrs, Set.add (UWeak (u,u')) soft
       | Covariant when cv_pb == Reduction.CUMUL ->
         Univ.Constraint.add (u,Univ.Le,u') cstrs, soft
       | Covariant | Invariant -> Univ.Constraint.add (u,Univ.Eq,u') cstrs, soft)
@@ -834,10 +882,10 @@ let compare_cumulative_instances cv_pb variances u u' sigma =
   | exception Univ.UniverseInconsistency p -> Inr p
 
 let compare_constructor_instances evd u u' =
-  let open Universes in
+  let open UnivProblem in
   let soft =
-    Array.fold_left2 (fun cs u u' -> Constraints.add (UWeak (u,u')) cs)
-      Constraints.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u')
+    Array.fold_left2 (fun cs u u' -> Set.add (UWeak (u,u')) cs)
+      Set.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u')
   in
   Evd.add_universe_constraints evd soft
 
@@ -849,17 +897,16 @@ let compare_constructor_instances evd u u' =
 let eq_constr_univs_test sigma1 sigma2 t u =
   (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *)
   let open Evd in
+  let t = EConstr.Unsafe.to_constr t
+  and u = EConstr.Unsafe.to_constr u in
   let fold cstr sigma =
     try Some (add_universe_constraints sigma cstr)
     with Univ.UniverseInconsistency _ | UniversesDiffer -> None
   in
   let ans =
-    Universes.eq_constr_univs_infer_with
+    UnivProblem.eq_constr_univs_infer_with
       (fun t -> kind_of_term_upto sigma1 t)
       (fun u -> kind_of_term_upto sigma2 u)
       (universes sigma2) fold t u sigma2
   in
   match ans with None -> false | Some _ -> true
-
-type type_constraint = EConstr.types option
-type val_constraint = EConstr.constr option
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index e289ca16..0ad323ac 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -12,6 +12,7 @@ open Names
 open Constr
 open Evd
 open Environ
+open Namegen
 open EConstr
 
 (** This module provides useful higher-level functions for evar manipulation. *)
@@ -25,53 +26,48 @@ val mk_new_meta : unit -> constr
 (** {6 Creating a fresh evar given their type and context} *)
 
 val new_evar_from_context :
-  named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+  ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> types -> evar_map * EConstr.t
+  ?naming:intro_pattern_naming_expr ->
+  ?principal:bool ->
+  named_context_val -> evar_map  -> types -> evar_map * EConstr.t
+
+type naming_mode =
+  | KeepUserNameAndRenameExistingButSectionNames
+  | KeepUserNameAndRenameExistingEvenSectionNames
+  | KeepExistingNames
+  | FailIfConflict
 
 val new_evar :
-  env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+  ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> types -> evar_map * EConstr.t
+  ?naming:intro_pattern_naming_expr ->
+  ?principal:bool -> ?hypnaming:naming_mode ->
+  env -> evar_map -> types -> evar_map * EConstr.t
 
 val new_pure_evar :
-  named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+  ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> types -> evar_map * Evar.t
+  ?naming:intro_pattern_naming_expr ->
+  ?principal:bool ->
+  named_context_val -> evar_map -> types -> evar_map * Evar.t
 
 val new_pure_evar_full : evar_map -> evar_info -> evar_map * Evar.t
 
-(** the same with side-effects *)
-val e_new_evar :
-  env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
-  ?candidates:constr list -> ?store:Store.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> types -> constr
-
 (** Create a new Type existential variable, as we keep track of 
     them during type-checking and unification. *)
 val new_type_evar :
-  env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid ->
-  evar_map * (constr * Sorts.t)
-
-val e_new_type_evar : env -> evar_map ref ->
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * Sorts.t
-
-val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr
-val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
+  ?naming:intro_pattern_naming_expr ->
+  ?principal:bool -> ?hypnaming:naming_mode ->
+  env -> evar_map -> rigid ->
+  evar_map * (constr * Sorts.t)
 
-val restrict_evar : evar_map -> Evar.t -> Filter.t ->
-  ?src:Evar_kinds.t Loc.located -> constr list option -> evar_map * Evar.t
+val new_Type : ?rigid:rigid -> evar_map -> evar_map * constr
 
 (** Polymorphic constants *)
 
-val new_global : evar_map -> Globnames.global_reference -> evar_map * constr
-val e_new_global : evar_map ref -> Globnames.global_reference -> constr
+val new_global : evar_map -> GlobRef.t -> evar_map * constr
 
 (** Create a fresh evar in a context different from its definition context:
    [new_evar_instance sign evd ty inst] creates a new evar of context
@@ -80,10 +76,10 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> constr
    of [inst] are typed in the occurrence context and their type (seen
    as a telescope) is [sign] *)
 val new_evar_instance :
- named_context_val -> evar_map -> types -> 
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list ->
-  ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr ->
+  ?store:Store.t -> ?naming:intro_pattern_naming_expr ->
   ?principal:bool ->
+ named_context_val -> evar_map -> types ->
   constr list -> evar_map * constr
 
 val make_pure_subst : evar_info -> 'a array -> (Id.t * 'a) list
@@ -132,7 +128,7 @@ val advance : evar_map -> Evar.t -> Evar.t option
     [nf_evar]. *)
 
 val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t
-val undefined_evars_of_named_context : evar_map -> Context.Named.t -> Evar.Set.t
+val undefined_evars_of_named_context : evar_map -> Constr.named_context -> Evar.Set.t
 val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t
 
 type undefined_evars_cache
@@ -165,7 +161,7 @@ val jv_nf_evar :
 val tj_nf_evar :
    evar_map -> unsafe_type_judgment -> unsafe_type_judgment
 
-val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t
+val nf_named_context_evar : evar_map -> Constr.named_context -> Constr.named_context
 val nf_rel_context_evar : evar_map -> rel_context -> rel_context
 val nf_env_evar : evar_map -> env -> env
 
@@ -178,11 +174,12 @@ val nf_evar_map_undefined : evar_map -> evar_map
 val nf_evars_universes : evar_map -> Constr.constr -> Constr.constr
 
 val nf_evars_and_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr)
-val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * Universes.universe_opt_subst
+[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"]
 
 (** Normalize the evar map w.r.t. universes, after simplification of constraints.
     Return the substitution function for constrs as well. *)
 val nf_evar_map_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr)
+[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evar_map and nf_evars_universes"]
 
 (** Replacing all evars, possibly raising [Uninstantiated_evar] *)
 exception Uninstantiated_evar of Evar.t
@@ -201,7 +198,7 @@ val kind_of_term_upto : evar_map -> Constr.constr ->
     universes. The term [t] is interpreted in [sigma1] while [u] is
     interpreted in [sigma2]. The universe constraints in [sigma2] are
     assumed to be an extention of those in [sigma1]. *)
-val eq_constr_univs_test : evar_map -> evar_map -> Constr.constr -> Constr.constr -> bool
+val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool
 
 (** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns
    [Inl sigma'] where [sigma'] is [sigma] augmented with universe
@@ -217,20 +214,37 @@ val compare_cumulative_instances : Reduction.conv_pb -> Univ.Variance.t array ->
 val compare_constructor_instances : evar_map ->
   Univ.Instance.t -> Univ.Instance.t -> evar_map
 
+(** {6 Unification problems} *)
+type unification_pb = conv_pb * env * constr * constr
+
+(** [add_unification_pb ?tail pb sigma]
+    Add a unification problem [pb] to [sigma], if not already present.
+    Put it at the end of the list if [tail] is true, by default it is false. *)
+val add_unification_pb : ?tail:bool -> unification_pb -> evar_map -> evar_map
+
 (** {6 Removing hyps in evars'context}
 raise OccurHypInSimpleClause if the removal breaks dependencies *)
 
 type clear_dependency_error =
 | OccurHypInSimpleClause of Id.t option
 | EvarTypingBreak of Constr.existential
+| NoCandidatesLeft of Evar.t
+
+exception ClearDependencyError of Id.t * clear_dependency_error * GlobRef.t option
 
-exception ClearDependencyError of Id.t * clear_dependency_error
+(** Restrict an undefined evar according to a (sub)filter and candidates.
+    The evar will be defined if there is only one candidate left,
+@raise ClearDependencyError NoCandidatesLeft if the filter turns the candidates
+  into an empty list. *)
 
-val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types ->
-  Id.Set.t -> named_context_val * types
+val restrict_evar : evar_map -> Evar.t -> Filter.t ->
+  ?src:Evar_kinds.t Loc.located -> constr list option -> evar_map * Evar.t
 
-val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types ->
-  Id.Set.t -> named_context_val * types * types
+val clear_hyps_in_evi : env -> evar_map -> named_context_val -> types ->
+  Id.Set.t -> evar_map * named_context_val * types
+
+val clear_hyps2_in_evi : env -> evar_map -> named_context_val -> types -> types ->
+  Id.Set.t -> evar_map * named_context_val * types * types
 
 type csubst
 
@@ -240,10 +254,11 @@ val csubst_subst : csubst -> constr -> constr
 type ext_named_context =
   csubst * Id.Set.t * named_context
 
-val push_rel_decl_to_named_context :
+val push_rel_decl_to_named_context : ?hypnaming:naming_mode ->
   evar_map -> rel_declaration -> ext_named_context -> ext_named_context
 
-val push_rel_context_to_named_context : Environ.env -> evar_map -> types ->
+val push_rel_context_to_named_context : ?hypnaming:naming_mode ->
+  Environ.env -> evar_map -> types ->
   named_context_val * types * constr list * csubst
 
 val generalize_evar_over_rels : evar_map -> existential -> types * constr list
@@ -254,13 +269,29 @@ val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a
 val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a
 val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a
 
-val subterm_source : Evar.t -> Evar_kinds.t Loc.located ->
+val subterm_source : Evar.t -> ?where:Evar_kinds.subevar_kind -> Evar_kinds.t Loc.located ->
   Evar_kinds.t Loc.located
 
 val meta_counter_summary_tag : int Summary.Dyn.tag
 
-(** Deprecated *)
-type type_constraint = types option
-[@@ocaml.deprecated "use the version in Evardefine"]
-type val_constraint = constr option
-[@@ocaml.deprecated "use the version in Evardefine"]
+val e_new_evar :
+  env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+  ?candidates:constr list -> ?store:Store.t ->
+  ?naming:intro_pattern_naming_expr ->
+  ?principal:bool -> ?hypnaming:naming_mode -> types -> constr
+[@@ocaml.deprecated "Use [Evarutil.new_evar]"]
+
+val e_new_type_evar : env -> evar_map ref ->
+  ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+  ?naming:intro_pattern_naming_expr ->
+  ?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t
+[@@ocaml.deprecated "Use [Evarutil.new_type_evar]"]
+
+val e_new_Type : ?rigid:rigid -> evar_map ref -> constr
+[@@ocaml.deprecated "Use [Evarutil.new_Type]"]
+
+val e_new_global : evar_map ref -> GlobRef.t -> constr
+[@@ocaml.deprecated "Use [Evarutil.new_global]"]
+
+val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * UnivSubst.universe_opt_subst
+[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"]
diff --git a/engine/evd.ml b/engine/evd.ml
index f6e13e1f..a438e059 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -21,6 +21,9 @@ open Environ
 (* module RelDecl = Context.Rel.Declaration *)
 module NamedDecl = Context.Named.Declaration
 
+type econstr = constr
+type etypes = types
+
 (** Generic filters *)
 module Filter :
 sig
@@ -129,8 +132,6 @@ end
 
 module Store = Store.Make ()
 
-type evar = Evar.t
-
 let string_of_existential evk = "?X" ^ string_of_int (Evar.repr evk)
 
 type evar_body =
@@ -170,6 +171,8 @@ let evar_context evi = named_context_of_val evi.evar_hyps
 let evar_filtered_context evi =
   Filter.filter_list (evar_filter evi) (evar_context evi)
 
+let evar_candidates evi = evi.evar_candidates
+
 let evar_hyps evi = evi.evar_hyps
 
 let evar_filtered_hyps evi = match Filter.repr (evar_filter evi) with
@@ -507,8 +510,8 @@ let raw_map f d =
     in
     ans
   in
-  let defn_evars = EvMap.smartmapi f d.defn_evars in
-  let undf_evars = EvMap.smartmapi f d.undf_evars in
+  let defn_evars = EvMap.Smart.mapi f d.defn_evars in
+  let undf_evars = EvMap.Smart.mapi f d.undf_evars in
   { d with defn_evars; undf_evars; }
 
 let raw_map_undefined f d =
@@ -521,7 +524,7 @@ let raw_map_undefined f d =
     in
     ans
   in
-  { d with undf_evars = EvMap.smartmapi f d.undf_evars; }
+  { d with undf_evars = EvMap.Smart.mapi f d.undf_evars; }
 
 let is_evar = mem
 
@@ -537,10 +540,14 @@ let existential_value d (n, args) =
   | Evar_empty ->
     raise NotInstantiatedEvar
 
+let existential_value0 = existential_value
+
 let existential_opt_value d ev =
   try Some (existential_value d ev)
   with NotInstantiatedEvar -> None
 
+let existential_opt_value0 = existential_opt_value
+
 let existential_type d (n, args) =
   let info =
     try find d n
@@ -548,6 +555,8 @@ let existential_type d (n, args) =
       anomaly (str "Evar " ++ str (string_of_existential n) ++ str " was not declared.") in
   instantiate_evar_array info info.evar_concl args
 
+let existential_type0 = existential_type
+
 let add_constraints d c =
   { d with universes = UState.add_constraints d.universes c }
 
@@ -613,11 +622,13 @@ let merge_universe_context evd uctx' =
 let set_universe_context evd uctx' =
   { evd with universes = uctx' }
 
+(* TODO: make unique *)
 let add_conv_pb ?(tail=false) pb d =
-  (** MS: we have duplicates here, why? *)
   if tail then {d with conv_pbs = d.conv_pbs @ [pb]}
   else {d with conv_pbs = pb::d.conv_pbs}
 
+let conv_pbs d = d.conv_pbs
+
 let evar_source evk d = (find d evk).evar_source
 
 let evar_ident evk evd = EvNames.ident evk evd.evar_names
@@ -763,7 +774,7 @@ let universe_subst evd =
   UState.subst evd.universes
 
 let merge_context_set ?loc ?(sideff=false) rigid evd ctx' =
-  {evd with universes = UState.merge ?loc sideff rigid evd.universes ctx'}
+  {evd with universes = UState.merge ?loc ~sideff ~extend:true rigid evd.universes ctx'}
 
 let merge_universe_subst evd subst = 
   {evd with universes = UState.merge_subst evd.universes subst }
@@ -794,22 +805,20 @@ let make_flexible_variable evd ~algebraic u =
 (* Operations on constants              *)
 (****************************************)
 
-let fresh_sort_in_family ?loc ?(rigid=univ_flexible) env evd s = 
-  with_context_set ?loc rigid evd (Universes.fresh_sort_in_family env s)
+let fresh_sort_in_family ?loc ?(rigid=univ_flexible) evd s =
+  with_context_set ?loc rigid evd (UnivGen.fresh_sort_in_family s)
 
 let fresh_constant_instance ?loc env evd c =
-  with_context_set ?loc univ_flexible evd (Universes.fresh_constant_instance env c)
+  with_context_set ?loc univ_flexible evd (UnivGen.fresh_constant_instance env c)
 
 let fresh_inductive_instance ?loc env evd i =
-  with_context_set ?loc univ_flexible evd (Universes.fresh_inductive_instance env i)
+  with_context_set ?loc univ_flexible evd (UnivGen.fresh_inductive_instance env i)
 
 let fresh_constructor_instance ?loc env evd c =
-  with_context_set ?loc univ_flexible evd (Universes.fresh_constructor_instance env c)
+  with_context_set ?loc univ_flexible evd (UnivGen.fresh_constructor_instance env c)
 
 let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
-  with_context_set ?loc rigid evd (Universes.fresh_global_instance ?names env gr)
-
-let whd_sort_variable evd t = t
+  with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?names env gr)
 
 let is_sort_variable evd s = UState.is_sort_variable evd.universes s
 
@@ -833,18 +842,18 @@ let universe_rigidity evd l =
   else UnivRigid
 
 let normalize_universe evd =
-  let vars = ref (UState.subst evd.universes) in
-  let normalize = Universes.normalize_universe_opt_subst vars in
+  let vars = UState.subst evd.universes in
+  let normalize = UnivSubst.normalize_universe_opt_subst vars in
     normalize
 
 let normalize_universe_instance evd l =
-  let vars = ref (UState.subst evd.universes) in
-  let normalize = Universes.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in
+  let vars = UState.subst evd.universes in
+  let normalize = UnivSubst.level_subst_of (UnivSubst.normalize_univ_variable_opt_subst vars) in
     Univ.Instance.subst_fn normalize l
 
 let normalize_sort evars s =
   match s with
-  | Prop _ -> s
+  | Prop | Set -> s
   | Type u -> 
     let u' = normalize_universe evars u in
     if u' == u then s else Type u'
@@ -857,7 +866,7 @@ let set_eq_sort env d s1 s2 =
   | Some (u1, u2) ->
     if not (type_in_type env) then
       add_universe_constraints d
-        (Universes.Constraints.singleton (Universes.UEq (u1,u2)))
+        (UnivProblem.Set.singleton (UnivProblem.UEq (u1,u2)))
     else
       d
 
@@ -869,7 +878,7 @@ let set_leq_level d u1 u2 =
 
 let set_eq_instances ?(flex=false) d u1 u2 =
   add_universe_constraints d
-    (Universes.enforce_eq_instances_univs flex u1 u2 Universes.Constraints.empty)
+    (UnivProblem.enforce_eq_instances_univs flex u1 u2 UnivProblem.Set.empty)
 
 let set_leq_sort env evd s1 s2 =
   let s1 = normalize_sort evd s1 
@@ -878,7 +887,7 @@ let set_leq_sort env evd s1 s2 =
   | None -> evd
   | Some (u1, u2) ->
      if not (type_in_type env) then
-       add_universe_constraints evd (Universes.Constraints.singleton (Universes.ULe (u1,u2)))
+       add_universe_constraints evd (UnivProblem.Set.singleton (UnivProblem.ULe (u1,u2)))
      else evd
 	    
 let check_eq evd s s' =
@@ -887,6 +896,9 @@ let check_eq evd s s' =
 let check_leq evd s s' =
   UGraph.check_leq (UState.ugraph evd.universes) s s'
 
+let check_constraints evd csts =
+  UGraph.check_constraints csts (UState.ugraph evd.universes)
+
 let fix_undefined_variables evd =
   { evd with universes = UState.fix_undefined_variables evd.universes }
 
@@ -1031,11 +1043,11 @@ let map_metas_fvalue f evd =
   | Clval(id,(c,s),typ) -> Clval(id,(mk_freelisted (f c.rebus),s),typ)
   | x -> x
   in
-  set_metas evd (Metamap.smartmap map evd.metas)
+  set_metas evd (Metamap.Smart.map map evd.metas)
 
 let map_metas f evd =
   let map cl = map_clb f cl in
-  set_metas evd (Metamap.smartmap map evd.metas)
+  set_metas evd (Metamap.Smart.map map evd.metas)
 
 let meta_opt_fvalue evd mv =
   match Metamap.find mv evd.metas with
@@ -1065,6 +1077,7 @@ let meta_ftype evd mv =
     | Clval(_,_,b) -> b
 
 let meta_type evd mv = (meta_ftype evd mv).rebus
+let meta_type0 = meta_type
 
 let meta_declare mv v ?(name=Anonymous) evd =
   let metas = Metamap.add mv (Cltyp(name,mk_freelisted v)) evd.metas in
@@ -1110,7 +1123,7 @@ let retract_coercible_metas evd =
     Cltyp (na, typ)
   | v -> v
   in
-  let metas = Metamap.smartmapi map evd.metas in
+  let metas = Metamap.Smart.mapi map evd.metas in
   !mc, set_metas evd metas
 
 let evar_source_of_meta mv evd =
@@ -1196,24 +1209,75 @@ module Monad =
 
 type unsolvability_explanation = SeveralInstancesFound of int
 
-(** Deprecated *)
-type evar_universe_context = UState.t
-let empty_evar_universe_context = UState.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 constrain_variables = UState.constrain_variables
-let evar_universe_context_of_binders = UState.of_binders
-let make_evar_universe_context e l =
-  let g = Environ.universes e in
-  match l with
-  | None -> UState.make g
-  | Some l -> UState.make_with_initial_binders g l
-let normalize_evar_universe_context_variables = UState.normalize_variables
-let abstract_undefined_variables = UState.abstract_undefined_variables
-let normalize_evar_universe_context = UState.minimize
-let nf_constraints = minimize_universes
+module MiniEConstr = struct
+
+  module ESorts =
+  struct
+    type t = Sorts.t
+    let make s = s
+    let kind sigma = function
+      | Sorts.Type u -> Sorts.sort_of_univ (normalize_universe sigma u)
+      | s -> s
+    let unsafe_to_sorts s = s
+  end
+
+  module EInstance =
+  struct
+    type t = Univ.Instance.t
+    let make i = i
+    let kind sigma i =
+      if Univ.Instance.is_empty i then i
+      else normalize_universe_instance sigma i
+    let empty = Univ.Instance.empty
+    let is_empty = Univ.Instance.is_empty
+    let unsafe_to_instance t = t
+  end
+
+  type t = econstr
+
+  let safe_evar_value sigma ev =
+    try Some (existential_value sigma ev)
+    with NotInstantiatedEvar | Not_found -> None
+
+  let rec whd_evar sigma c =
+    match Constr.kind c with
+    | Evar ev ->
+      begin match safe_evar_value sigma ev with
+        | Some c -> whd_evar sigma c
+        | None -> c
+      end
+    | App (f, args) when isEvar f ->
+      (** Enforce smart constructor invariant on applications *)
+      let ev = destEvar f in
+      begin match safe_evar_value sigma ev with
+        | None -> c
+        | Some f -> whd_evar sigma (mkApp (f, args))
+      end
+    | Cast (c0, k, t) when isEvar c0 ->
+      (** Enforce smart constructor invariant on casts. *)
+      let ev = destEvar c0 in
+      begin match safe_evar_value sigma ev with
+        | None -> c
+        | Some c -> whd_evar sigma (mkCast (c, k, t))
+      end
+    | _ -> c
+
+  let kind sigma c = Constr.kind (whd_evar sigma c)
+  let kind_upto = kind
+  let kind_of_type sigma c = Term.kind_of_type (whd_evar sigma c)
+  let of_kind = Constr.of_kind
+  let of_constr c = c
+  let unsafe_to_constr c = c
+  let unsafe_eq = Refl
+
+  let to_constr ?(abort_on_undefined_evars=true) sigma c =
+    let evar_value ev = safe_evar_value sigma ev in
+    UnivSubst.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c
+
+  let of_named_decl d = d
+  let unsafe_to_named_decl d = d
+  let of_rel_decl d = d
+  let unsafe_to_rel_decl d = d
+  let to_rel_decl sigma d = Context.Rel.Declaration.map_constr (to_constr sigma) d
+
+end
diff --git a/engine/evd.mli b/engine/evd.mli
index 911799c4..db2bd4ee 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -28,15 +28,10 @@ open Environ
     It also contains conversion constraints, debugging information and
     information about meta variables. *)
 
-(** {5 Existential variables and unification states} *)
-
-type evar = Evar.t
-[@@ocaml.deprecated "use Evar.t"]
-(** Existential variables. *)
+type econstr
+type etypes = econstr
 
-(** {6 Evars} *)
-val string_of_existential : Evar.t -> string
-[@@ocaml.deprecated "use Evar.print"]
+(** {5 Existential variables and unification states} *)
 
 (** {6 Evar filters} *)
 
@@ -86,16 +81,16 @@ end
 
 type evar_body =
   | Evar_empty
-  | Evar_defined of constr
+  | Evar_defined of econstr
 
 
 module Store : Store.S
 (** Datatype used to store additional information in evar maps. *)
 
 type evar_info = {
-  evar_concl : constr;
+  evar_concl : econstr;
   (** Type of the evar. *)
-  evar_hyps : named_context_val;
+  evar_hyps : named_context_val; (** TODO econstr? *)
   (** Context of the evar. *)
   evar_body : evar_body;
   (** Optional content of the evar. *)
@@ -105,32 +100,29 @@ type evar_info = {
       in the solution *)
   evar_source : Evar_kinds.t located;
   (** Information about the evar. *)
-  evar_candidates : constr list option;
+  evar_candidates : econstr list option;
   (** List of possible solutions when known that it is a finite list *)
   evar_extra : Store.t
   (** Extra store, used for clever hacks. *)
 }
 
-val make_evar : named_context_val -> types -> evar_info
-val evar_concl : evar_info -> constr
-val evar_context : evar_info -> Context.Named.t
-val evar_filtered_context : evar_info -> Context.Named.t
+val make_evar : named_context_val -> etypes -> evar_info
+val evar_concl : evar_info -> econstr
+val evar_context : evar_info -> (econstr, etypes) Context.Named.pt
+val evar_filtered_context : evar_info -> (econstr, etypes) Context.Named.pt
 val evar_hyps : evar_info -> named_context_val
 val evar_filtered_hyps : evar_info -> named_context_val
 val evar_body : evar_info -> evar_body
+val evar_candidates : evar_info -> constr list option
 val evar_filter : evar_info -> Filter.t
 val evar_env :  evar_info -> env
 val evar_filtered_env :  evar_info -> env
 
-val map_evar_body : (constr -> constr) -> evar_body -> evar_body
-val map_evar_info : (constr -> constr) -> evar_info -> evar_info
+val map_evar_body : (econstr -> econstr) -> evar_body -> evar_body
+val map_evar_info : (econstr -> econstr) -> evar_info -> evar_info
 
 (** {6 Unification state} **)
 
-type evar_universe_context = UState.t
-[@@ocaml.deprecated "Alias of UState.t"]
-(** The universe context associated to an evar map *)
-
 type evar_map
 (** Type of unification state. Essentially a bunch of state-passing data needed
     to handle incremental term construction. *)
@@ -190,7 +182,7 @@ val raw_map_undefined : (Evar.t -> evar_info -> evar_info) -> evar_map -> evar_m
 (** Same as {!raw_map}, but restricted to undefined evars. For efficiency
     reasons. *)
 
-val define : Evar.t-> constr -> evar_map -> evar_map
+val define : Evar.t-> econstr -> evar_map -> evar_map
 (** Set the body of an evar to the given constr. It is expected that:
     {ul
       {- The evar is already present in the evarmap.}
@@ -198,7 +190,7 @@ val define : Evar.t-> constr -> evar_map -> evar_map
       {- All the evars present in the constr should be present in the evar map.}
     } *)
 
-val cmap : (constr -> constr) -> evar_map -> evar_map
+val cmap : (econstr -> econstr) -> evar_map -> evar_map
 (** Map the function on all terms in the evar map. *)
 
 val is_evar : evar_map -> Evar.t-> bool
@@ -222,20 +214,26 @@ val drop_all_defined : evar_map -> evar_map
 
 exception NotInstantiatedEvar
 
-val existential_value : evar_map -> existential -> constr
+val existential_value : evar_map -> econstr pexistential -> econstr
 (** [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has
     no body and [Not_found] if it does not exist in [sigma] *)
 
-val existential_type : evar_map -> existential -> types
+val existential_value0 : evar_map -> existential -> constr
+
+val existential_type : evar_map -> econstr pexistential -> etypes
+
+val existential_type0 : evar_map -> existential -> types
 
-val existential_opt_value : evar_map -> existential -> constr option
+val existential_opt_value : evar_map -> econstr pexistential -> econstr option
 (** Same as {!existential_value} but returns an option instead of raising an
     exception. *)
 
-val evar_instance_array : (Context.Named.Declaration.t -> 'a -> bool) -> evar_info ->
+val existential_opt_value0 : evar_map -> existential -> constr option
+
+val evar_instance_array : (Constr.named_declaration -> 'a -> bool) -> evar_info ->
   'a array -> (Id.t * 'a) list
 
-val instantiate_evar_array : evar_info -> constr -> constr array -> constr
+val instantiate_evar_array : evar_info -> econstr -> econstr array -> econstr
 
 val evars_reset_evd  : ?with_conv_pbs:bool -> ?with_univs:bool -> 
   evar_map ->  evar_map -> evar_map
@@ -243,15 +241,16 @@ val evars_reset_evd  : ?with_conv_pbs:bool -> ?with_univs:bool ->
 
 (** {6 Misc} *)
 
-val restrict : Evar.t-> Filter.t -> ?candidates:constr list ->
+val restrict : Evar.t-> Filter.t -> ?candidates:econstr list ->
   ?src:Evar_kinds.t located -> evar_map -> evar_map * Evar.t
 (** Restrict an undefined evar into a new evar by filtering context and
-    possibly limiting the instances to a set of candidates *)
+    possibly limiting the instances to a set of candidates (candidates
+    are filtered according to the filter) *)
 
 val is_restricted_evar : evar_info -> Evar.t option
 (** Tell if an evar comes from restriction of another evar, and if yes, which *)
 
-val downcast : Evar.t-> types -> evar_map -> evar_map
+val downcast : Evar.t-> etypes -> evar_map -> evar_map
 (** Change the type of an undefined evar to a new type assumed to be a
     subtype of its current type; subtyping must be ensured by caller *)
 
@@ -341,11 +340,9 @@ val shelve_on_future_goals : Evar.t list -> future_goals -> future_goals
     Evar maps also keep track of the universe constraints defined at a given
     point. This section defines the relevant manipulation functions. *)
 
-val whd_sort_variable : evar_map -> constr -> constr
-
 exception UniversesDiffer
 
-val add_universe_constraints : evar_map -> Universes.Constraints.t -> evar_map
+val add_universe_constraints : evar_map -> UnivProblem.Set.t -> evar_map
 (** Add the given universe unification constraints to the evar map.
     @raise UniversesDiffer in case a first-order unification fails.
     @raise UniverseInconsistency .
@@ -397,8 +394,8 @@ type 'a freelisted = {
   rebus : 'a;
   freemetas : Metaset.t }
 
-val metavars_of : constr -> Metaset.t
-val mk_freelisted : constr -> constr freelisted
+val metavars_of : econstr -> Metaset.t
+val mk_freelisted : econstr -> econstr freelisted
 val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted
 
 (** Status of an instance found by unification wrt to the meta it solves:
@@ -436,13 +433,17 @@ type instance_status = instance_constraint * instance_typing_status
 (** Clausal environments *)
 
 type clbinding =
-  | Cltyp of Name.t * constr freelisted
-  | Clval of Name.t * (constr freelisted * instance_status) * constr freelisted
+  | Cltyp of Name.t * econstr freelisted
+  | Clval of Name.t * (econstr freelisted * instance_status) * econstr freelisted
 
 (** Unification constraints *)
 type conv_pb = Reduction.conv_pb
-type evar_constraint = conv_pb * env * constr * constr
+type evar_constraint = conv_pb * env * econstr * econstr
+
+(** The following two functions are for internal use only,
+    see [Evarutil.add_unification_pb] for a safe interface. *)
 val add_conv_pb : ?tail:bool -> evar_constraint -> evar_map -> evar_map
+val conv_pbs : evar_map -> evar_constraint list
 
 val extract_changed_conv_pbs : evar_map ->
       (Evar.Set.t -> evar_constraint -> bool) ->
@@ -457,7 +458,7 @@ val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option
 val evars_of_term : constr -> Evar.Set.t
   (** including evars in instances of evars *)
 
-val evars_of_named_context : Context.Named.t -> Evar.Set.t
+val evars_of_named_context : (econstr, etypes) Context.Named.pt -> Evar.Set.t
 
 val evars_of_filtered_evar_info : evar_info -> Evar.Set.t
 
@@ -465,19 +466,20 @@ val evars_of_filtered_evar_info : evar_info -> Evar.Set.t
 val meta_list : evar_map -> (metavariable * clbinding) list
 val meta_defined : evar_map -> metavariable -> bool
 
-val meta_value     : evar_map -> metavariable -> constr
+val meta_value     : evar_map -> metavariable -> econstr
 (** [meta_fvalue] raises [Not_found] if meta not in map or [Anomaly] if
    meta has no value *)
 
-val meta_fvalue    : evar_map -> metavariable -> constr freelisted * instance_status
-val meta_opt_fvalue : evar_map -> metavariable -> (constr freelisted * instance_status) option
-val meta_type      : evar_map -> metavariable -> types
-val meta_ftype     : evar_map -> metavariable -> types freelisted
+val meta_fvalue    : evar_map -> metavariable -> econstr freelisted * instance_status
+val meta_opt_fvalue : evar_map -> metavariable -> (econstr freelisted * instance_status) option
+val meta_type      : evar_map -> metavariable -> etypes
+val meta_type0 : evar_map -> metavariable -> types
+val meta_ftype     : evar_map -> metavariable -> etypes freelisted
 val meta_name      : evar_map -> metavariable -> Name.t
 val meta_declare   :
-  metavariable -> types -> ?name:Name.t -> evar_map -> evar_map
-val meta_assign    : metavariable -> constr * instance_status -> evar_map -> evar_map
-val meta_reassign  : metavariable -> constr * instance_status -> evar_map -> evar_map
+  metavariable -> etypes -> ?name:Name.t -> evar_map -> evar_map
+val meta_assign    : metavariable -> econstr * instance_status -> evar_map -> evar_map
+val meta_reassign  : metavariable -> econstr * instance_status -> evar_map -> evar_map
 
 val clear_metas : evar_map -> evar_map
 
@@ -485,10 +487,10 @@ val clear_metas : evar_map -> evar_map
 val meta_merge : ?with_univs:bool -> evar_map -> evar_map -> evar_map
 
 val undefined_metas : evar_map -> metavariable list
-val map_metas_fvalue : (constr -> constr) -> evar_map -> evar_map
-val map_metas : (constr -> constr) -> evar_map -> evar_map
+val map_metas_fvalue : (econstr -> econstr) -> evar_map -> evar_map
+val map_metas : (econstr -> econstr) -> evar_map -> evar_map
 
-type metabinding = metavariable * constr * instance_status
+type metabinding = metavariable * econstr * instance_status
 
 val retract_coercible_metas : evar_map -> metabinding list * evar_map
 
@@ -519,48 +521,11 @@ val univ_flexible_alg : rigid
 
 type 'a in_evar_universe_context = 'a * UState.t
 
-val evar_universe_context_set : UState.t -> Univ.ContextSet.t
-[@@ocaml.deprecated "Alias of UState.context_set"]
-val evar_universe_context_constraints : UState.t -> Univ.Constraint.t
-[@@ocaml.deprecated "Alias of UState.constraints"]
-val evar_context_universe_context : UState.t -> Univ.UContext.t
-[@@ocaml.deprecated "alias of UState.context"]
-
-val evar_universe_context_of : Univ.ContextSet.t -> UState.t
-[@@ocaml.deprecated "Alias of UState.of_context_set"]
-val empty_evar_universe_context : UState.t
-[@@ocaml.deprecated "Alias of UState.empty"]
-val union_evar_universe_context : UState.t -> UState.t ->
-  UState.t
-[@@ocaml.deprecated "Alias of UState.union"]
-val evar_universe_context_subst : UState.t -> Universes.universe_opt_subst
-[@@ocaml.deprecated "Alias of UState.subst"]
-val constrain_variables : Univ.LSet.t -> UState.t -> UState.t
-[@@ocaml.deprecated "Alias of UState.constrain_variables"]
-
-
-val evar_universe_context_of_binders :
-  Universes.universe_binders -> UState.t
-[@@ocaml.deprecated "Alias of UState.of_binders"]
-
-val make_evar_universe_context : env -> Misctypes.lident list option -> UState.t
-[@@ocaml.deprecated "Use UState.make or UState.make_with_initial_binders"]
 val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map
 (** Raises Not_found if not a name for a universe in this map. *)
 val universe_of_name : evar_map -> Id.t -> Univ.Level.t
 
-val universe_binders : evar_map -> Universes.universe_binders
-val add_constraints_context : UState.t ->
-  Univ.Constraint.t -> UState.t
-[@@ocaml.deprecated "Alias of UState.add_constraints"]
-
-
-val normalize_evar_universe_context_variables : UState.t -> 
-  Univ.universe_subst in_evar_universe_context
-[@@ocaml.deprecated "Alias of UState.normalize_variables"]
-
-val normalize_evar_universe_context : UState.t -> UState.t
-[@@ocaml.deprecated "Alias of UState.minimize"]
+val universe_binders : evar_map -> UnivNames.universe_binders
 
 val new_univ_level_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Level.t
 val new_univ_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Universe.t
@@ -591,9 +556,11 @@ val set_eq_instances : ?flex:bool ->
 val check_eq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
 val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
 
+val check_constraints : evar_map -> Univ.Constraint.t -> bool
+
 val evar_universe_context : evar_map -> UState.t
 val universe_context_set : evar_map -> Univ.ContextSet.t
-val universe_subst : evar_map -> Universes.universe_opt_subst
+val universe_subst : evar_map -> UnivSubst.universe_opt_subst
 val universes : evar_map -> UGraph.t
 
 (** [to_universe_context evm] extracts the local universes and
@@ -612,13 +579,11 @@ val merge_universe_context : evar_map -> UState.t -> evar_map
 val set_universe_context : evar_map -> UState.t -> evar_map
 
 val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.ContextSet.t -> evar_map
-val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map
+val merge_universe_subst : evar_map -> UnivSubst.universe_opt_subst -> evar_map
 
 val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a
 
 val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst
-val abstract_undefined_variables : UState.t -> UState.t
-[@@ocaml.deprecated "Alias of UState.abstract_undefined_variables"]
 
 val fix_undefined_variables : evar_map -> evar_map
 
@@ -626,26 +591,24 @@ val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_sub
 
 (** Universe minimization *)
 val minimize_universes : evar_map -> evar_map
-val nf_constraints : evar_map -> evar_map
-[@@ocaml.deprecated "Alias of Evd.minimize_universes"]
 
 val update_sigma_env : evar_map -> env -> evar_map
 
 (** Polymorphic universes *)
 
-val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> env -> evar_map -> Sorts.family -> evar_map * Sorts.t
+val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> evar_map -> Sorts.family -> evar_map * Sorts.t
 val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> Constant.t -> evar_map * pconstant
 val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive
 val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor
 
 val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env ->
-  evar_map -> Globnames.global_reference -> evar_map * constr
+  evar_map -> GlobRef.t -> evar_map * econstr
 
 (********************************************************************)
 (* constr with holes and pending resolution of classes, conversion  *)
 (* problems, candidates, etc.                                       *)
 
-type open_constr = evar_map * constr (* Special case when before is empty *)
+type open_constr = evar_map * econstr (* Special case when before is empty *)
 
 (** Partially constructed constrs. *)
 
@@ -665,3 +628,50 @@ val create_evar_defs : evar_map -> evar_map
 
 (** Create an [evar_map] with empty meta map: *)
 
+(** Use this module only to bootstrap EConstr *)
+module MiniEConstr : sig
+  module ESorts : sig
+    type t
+    val make : Sorts.t -> t
+    val kind : evar_map -> t -> Sorts.t
+    val unsafe_to_sorts : t -> Sorts.t
+  end
+
+  module EInstance : sig
+    type t
+    val make : Univ.Instance.t -> t
+    val kind : evar_map -> t -> Univ.Instance.t
+    val empty : t
+    val is_empty : t -> bool
+    val unsafe_to_instance : t -> Univ.Instance.t
+  end
+
+  type t = econstr
+
+  val kind : evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term
+  val kind_upto : evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term
+  val kind_of_type : evar_map -> t -> (t, t) Term.kind_of_type
+
+  val whd_evar : evar_map -> t -> t
+
+  val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t
+
+  val of_constr : Constr.t -> t
+
+  val to_constr : ?abort_on_undefined_evars:bool -> evar_map -> t -> Constr.t
+
+  val unsafe_to_constr : t -> Constr.t
+
+  val unsafe_eq : (t, Constr.t) eq
+
+  val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt ->
+    (t, t) Context.Named.Declaration.pt
+  val unsafe_to_named_decl : (t, t) Context.Named.Declaration.pt ->
+    (Constr.t, Constr.types) Context.Named.Declaration.pt
+  val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt ->
+    (Constr.t, Constr.types) Context.Rel.Declaration.pt
+  val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt ->
+    (t, t) Context.Rel.Declaration.pt
+  val to_rel_decl : evar_map -> (t, t) Context.Rel.Declaration.pt ->
+    (Constr.t, Constr.types) Context.Rel.Declaration.pt
+end
diff --git a/engine/namegen.ml b/engine/namegen.ml
index d66b77b5..978f33b6 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -17,6 +17,7 @@
 open Util
 open Names
 open Term
+open Constr
 open Environ
 open EConstr
 open Vars
@@ -28,6 +29,18 @@ open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
 
+(** General evar naming using intro patterns  *)
+type intro_pattern_naming_expr =
+  | IntroIdentifier of Id.t
+  | IntroFresh of Id.t
+  | IntroAnonymous
+
+let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
+| IntroAnonymous, IntroAnonymous -> true
+| IntroIdentifier id1, IntroIdentifier id2 -> Names.Id.equal id1 id2
+| IntroFresh id1, IntroFresh id2 -> Names.Id.equal id1 id2
+| _ -> false
+
 (**********************************************************************)
 (* Conventional names *)
 
@@ -124,8 +137,9 @@ let lowercase_first_char id = (* First character of a constr *)
         s ^ Unicode.lowercase_first_char s'
 
 let sort_hdchar = function
-  | Prop(_) -> "P"
-  | Type(_) -> "T"
+  | Prop -> "P"
+  | Set -> "S"
+  | Type _ -> "T"
 
 let hdchar env sigma c =
   let rec hdrec k c =
diff --git a/engine/namegen.mli b/engine/namegen.mli
index 1b70ef68..a53c3a0d 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -15,6 +15,16 @@ open Environ
 open Evd
 open EConstr
 
+(** General evar naming using intro patterns  *)
+type intro_pattern_naming_expr =
+  | IntroIdentifier of Id.t
+  | IntroFresh of Id.t
+  | IntroAnonymous
+
+(** Equalities on [intro_pattern_naming] *)
+val intro_pattern_naming_eq :
+  intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool
+
 (*********************************************************************
    Conventional default names *)
 
diff --git a/engine/nameops.ml b/engine/nameops.ml
index 53969caf..15e20134 100644
--- a/engine/nameops.ml
+++ b/engine/nameops.ml
@@ -11,10 +11,6 @@
 open Util
 open Names
 
-(* Identifiers *)
-
-let pr_id id = Id.print id
-
 (* Utilities *)
 
 let code_of_0 = Char.code '0'
@@ -73,7 +69,7 @@ let root_of_id id =
    [bar0]  ↦ [bar1]
    [bar00] ↦ [bar01]
    [bar1]  ↦ [bar2]
-   [bar01] ↦ [bar01]
+   [bar01] ↦ [bar02]
    [bar9]  ↦ [bar10]
    [bar09] ↦ [bar10]
    [bar99] ↦ [bar100]
@@ -191,28 +187,6 @@ struct
 
 end
 
-open Name
-
-(* Compatibility *)
-let out_name = get_id
-let name_fold = fold_right
-let name_iter = iter
-let name_app = map
-let name_fold_map = fold_left_map
-let name_cons = cons
-let name_max = pick
-let pr_name = print
-
-let pr_lab l = Label.print l
-
 (* Metavariables *)
 let pr_meta = Pp.int
 let string_of_meta = string_of_int
-
-(* Deprecated *)
-open Libnames
-let default_library = default_library
-let coq_string = coq_string
-let coq_root = coq_root
-let default_root_prefix = default_root_prefix
-
diff --git a/engine/nameops.mli b/engine/nameops.mli
index 96842dfb..8a93fad8 100644
--- a/engine/nameops.mli
+++ b/engine/nameops.mli
@@ -94,47 +94,3 @@ end
 (** Metavariables *)
 val pr_meta : Constr.metavariable -> Pp.t
 val string_of_meta : Constr.metavariable -> string
-
-val out_name : Name.t -> Id.t
-[@@ocaml.deprecated "Same as [Name.get_id]"]
-
-val name_fold : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a
-[@@ocaml.deprecated "Same as [Name.fold_right]"]
-
-val name_iter : (Id.t -> unit) -> Name.t -> unit
-[@@ocaml.deprecated "Same as [Name.iter]"]
-
-val name_app : (Id.t -> Id.t) -> Name.t -> Name.t
-[@@ocaml.deprecated "Same as [Name.map]"]
-
-val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
-[@@ocaml.deprecated "Same as [Name.fold_left_map]"]
-
-val name_max : Name.t -> Name.t -> Name.t
-[@@ocaml.deprecated "Same as [Name.pick]"]
-
-val name_cons : Name.t -> Id.t list -> Id.t list
-[@@ocaml.deprecated "Same as [Name.cons]"]
-
-val pr_name : Name.t -> Pp.t
-[@@ocaml.deprecated "Same as [Name.print]"]
-
-val pr_id : Id.t -> Pp.t
-[@@ocaml.deprecated "Same as [Names.Id.print]"]
-
-val pr_lab : Label.t -> Pp.t
-[@@ocaml.deprecated "Same as [Names.Label.print]"]
-
-(** Deprecated stuff to libnames *)
-val default_library : DirPath.t
-[@@ocaml.deprecated "Same as [Libnames.default_library]"]
-
-val coq_root : module_ident (** "Coq" *)
-[@@ocaml.deprecated "Same as [Libnames.coq_root]"]
-
-val coq_string : string (** "Coq" *)
-[@@ocaml.deprecated "Same as [Libnames.coq_string]"]
-
-val default_root_prefix : DirPath.t
-[@@ocaml.deprecated "Same as [Libnames.default_root_prefix]"]
-
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 22271dd0..12d31e5f 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -39,15 +39,15 @@ let proofview p =
 
 let compact el ({ solution } as pv) =
   let nf c = Evarutil.nf_evar solution c in
-  let nf0 c = EConstr.Unsafe.to_constr (Evarutil.nf_evar solution (EConstr.of_constr c)) in
+  let nf0 c = EConstr.(to_constr solution (of_constr c)) in
   let size = Evd.fold (fun _ _ i -> i+1) solution 0 in
   let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in
   let pruned_solution = Evd.drop_all_defined solution in
   let apply_subst_einfo _ ei =
     Evd.({ ei with
-       evar_concl =  nf0 ei.evar_concl;
+       evar_concl =  nf ei.evar_concl;
        evar_hyps = Environ.map_named_val nf0 ei.evar_hyps;
-       evar_candidates = Option.map (List.map nf0) ei.evar_candidates }) in
+       evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in
   let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in
   let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in
   Feedback.msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size));
@@ -710,13 +710,19 @@ let partition_unifiable sigma l =
 (** Shelves the unifiable goals under focus, i.e. the goals which
     appear in other goals under focus (the unfocused goals are not
     considered). *)
-let shelve_unifiable =
+let shelve_unifiable_informative =
   let open Proof in
   Pv.get >>= fun initial ->
   let (u,n) = partition_unifiable initial.solution initial.comb in
   Comb.set n >>
   InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_unifiable")) >>
-  Shelf.modify (fun gls -> gls @ CList.map drop_state u)
+  let u = CList.map drop_state u in
+  Shelf.modify (fun gls -> gls @ u) >>
+  tclUNIT u
+
+let shelve_unifiable =
+  let open Proof in
+  shelve_unifiable_informative >>= fun _ -> tclUNIT ()
 
 (** [guard_no_unifiable] returns the list of unifiable goals if some
     goals are unifiable (see {!shelve_unifiable}) in the current focus. *)
@@ -748,7 +754,7 @@ let mark_in_evm ~goal evd content =
                - GoalEvar (morally not dependent)
                - VarInstance (morally dependent of some name).
                This is a heuristic for naming these evars. *)
-            | loc, (Evar_kinds.QuestionMark (_,Names.Name id) |
+  | loc, (Evar_kinds.QuestionMark { Evar_kinds.qm_name=Names.Name id} |
                     Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id
             | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
             | loc,_ -> loc,Evar_kinds.GoalEvar }
@@ -869,8 +875,7 @@ module Progress = struct
 
   (** equality function on hypothesis contexts *)
   let eq_named_context_val sigma1 sigma2 ctx1 ctx2 =
-    let open Environ in
-    let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in
+    let c1 = EConstr.named_context_of_val ctx1 and c2 = EConstr.named_context_of_val ctx2 in
     let eq_named_declaration d1 d2 =
       match d1, d2 with
       | LocalAssum (i1,t1), LocalAssum (i2,t2) ->
@@ -1035,6 +1040,8 @@ module Unsafe = struct
 
   let advance = Evarutil.advance
 
+  let undefined = undefined
+
   let mark_as_unresolvable p gl =
     { p with solution = mark_in_evm ~goal:false p.solution gl }
 
@@ -1078,8 +1085,6 @@ module Goal = struct
     self : Evar.t ; (* for compatibility with old-style definitions *)
   }
 
-  let assume (gl : t) = (gl : t)
-
   let print { sigma; self } = { Evd.it = self; sigma }
 
   let state { state=state } = state
@@ -1093,7 +1098,7 @@ module Goal = struct
   let gmake_with info env sigma goal state =
     { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ;
       sigma = sigma ;
-      concl = EConstr.of_constr (Evd.evar_concl info);
+      concl = Evd.evar_concl info;
       state = state ;
       self = goal }
 
@@ -1267,11 +1272,6 @@ module V82 = struct
       
     
 
-  (* Returns the open goals of the proofview together with the evar_map to 
-     interpret them. *)
-  let goals { comb = comb ; solution = solution; } =
-   { Evd.it = List.map drop_state comb ; sigma = solution }
-
   let top_goals initial { solution=solution; } =
     let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in
     { Evd.it = goals ; sigma=solution; }
diff --git a/engine/proofview.mli b/engine/proofview.mli
index e7be6655..970bf677 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -326,6 +326,9 @@ val unifiable : Evd.evar_map -> Evar.t -> Evar.t list -> bool
     considered). *)
 val shelve_unifiable : unit tactic
 
+(** Idem but also returns the list of shelved variables *)
+val shelve_unifiable_informative : Evar.t list tactic
+
 (** [guard_no_unifiable] returns the list of unifiable goals if some
     goals are unifiable (see {!shelve_unifiable}) in the current focus. *)
 val guard_no_unifiable : Names.Name.t list option tactic
@@ -466,6 +469,12 @@ module Unsafe : sig
       solved. *)
   val advance : Evd.evar_map -> Evar.t -> Evar.t option
 
+  (** [undefined sigma l] applies [advance] to the goals of [l], then
+      returns the subset of resulting goals which have not yet been
+      defined *)
+  val undefined : Evd.evar_map -> Proofview_monad.goal_with_state list ->
+    Proofview_monad.goal_with_state list
+
   val typeclass_resolvable : unit Evd.Store.field
 
 end
@@ -486,10 +495,6 @@ module Goal : sig
   (** Type of goals. *)
   type t
 
-  (** Assume that you do not need the goal to be normalized. *)
-  val assume : t -> t
-  [@@ocaml.deprecated "Normalization is enforced by EConstr, [assume] is not needed anymore"]
-
   (** Normalises the argument goal. *)
   val normalize : t -> t tactic
 
@@ -580,11 +585,6 @@ module V82 : sig
      (in chronological order of insertion). *)
   val grab : proofview -> proofview
 
-  (* Returns the open goals of the proofview together with the evar_map to 
-     interpret them. *)
-  val goals : proofview -> Evar.t list Evd.sigma
-  [@@ocaml.deprecated "Use [Proofview.proofview]"]
-
   val top_goals : entry -> proofview -> Evar.t list Evd.sigma
 
   (* returns the existential variable used to start the proof *)
diff --git a/engine/termops.ml b/engine/termops.ml
index 3dfb0c34..a343ad3c 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -22,11 +22,13 @@ module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 module CompactedDecl = Context.Compacted.Declaration
 
+module Internal = struct
+
 (* Sorts and sort family *)
 
 let print_sort = function
-  | Prop Pos -> (str "Set")
-  | Prop Null -> (str "Prop")
+  | Set -> (str "Set")
+  | Prop -> (str "Prop")
   | Type u -> (str "Type(" ++ Univ.Universe.pr u ++ str ")")
 
 let pr_sort_family = function
@@ -47,7 +49,9 @@ let pr_fix pr_constr ((t,i),(lna,tl,bl)) =
 
 let pr_puniverses p u = 
   if Univ.Instance.is_empty u then p 
-  else p ++ str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)"
+  else p ++ str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)"
+
+(* Minimalistic constr printer, typically for debugging *)
 
 let rec pr_constr c = match kind c with
   | Rel n -> str "#"++int n
@@ -96,9 +100,16 @@ let rec pr_constr c = match kind c with
            cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
          str"}")
 
-let term_printer = ref (fun _env _sigma c -> pr_constr (EConstr.Unsafe.to_constr c))
+let debug_print_constr c = pr_constr EConstr.Unsafe.(to_constr c)
+let debug_print_constr_env env sigma c = pr_constr EConstr.(to_constr sigma c)
+let term_printer = ref debug_print_constr_env
+
 let print_constr_env env sigma t = !term_printer env sigma t
-let print_constr t = !term_printer (Global.env()) Evd.empty t
+let print_constr t =
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+  !term_printer env evd t
+
 let set_print_constr f = term_printer := f
 
 module EvMap = Evar.Map
@@ -111,11 +122,11 @@ let pr_evar_suggested_name evk sigma =
   | None -> match evi.evar_source with
   | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
   | _,Evar_kinds.VarInstance id -> id
-  | _,Evar_kinds.QuestionMark (_,Name id) -> id
+  | _,Evar_kinds.QuestionMark {Evar_kinds.qm_name = Name id} -> id
   | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
   | _ ->
       let env = reset_with_named_context evi.evar_hyps (Global.env()) in
-      Namegen.id_of_name_using_hdchar env sigma (EConstr.of_constr evi.evar_concl) Anonymous
+      Namegen.id_of_name_using_hdchar env sigma evi.evar_concl Anonymous
   in
   let names = EvMap.mapi base_id (undefined_map sigma) in
   let id = EvMap.find evk names in
@@ -154,7 +165,7 @@ let protect f x =
   with e -> str "EXCEPTION: " ++ str (Printexc.to_string e)
 
 let print_kconstr a =
-  protect (fun c -> print_constr (EConstr.of_constr c)) a
+  protect (fun c -> print_constr c) a
 
 let pr_meta_map evd =
   let open Evd in
@@ -197,17 +208,21 @@ let pr_evar_source = function
       let print_constr = print_kconstr in
       let id = Option.get ido in
       str "parameter " ++ Id.print id ++ spc () ++ str "of" ++
-      spc () ++ print_constr (printable_constr_of_global c)
+      spc () ++ print_constr (EConstr.of_constr @@ printable_constr_of_global c)
   | Evar_kinds.InternalHole -> str "internal placeholder"
   | Evar_kinds.TomatchTypeParameter (ind,n) ->
       let print_constr = print_kconstr in
-      pr_nth n ++ str " argument of type " ++ print_constr (mkInd ind)
+      pr_nth n ++ str " argument of type " ++ print_constr (EConstr.mkInd ind)
   | Evar_kinds.GoalEvar -> str "goal evar"
   | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause"
   | Evar_kinds.MatchingVar _ -> str "matching variable"
   | Evar_kinds.VarInstance id -> str "instance of " ++ Id.print id
-  | Evar_kinds.SubEvar evk ->
-    str "subterm of " ++ Evar.print evk
+  | Evar_kinds.SubEvar (where,evk) ->
+     (match where with
+     | None -> str "subterm of "
+     | Some Evar_kinds.Body -> str "body of "
+     | Some Evar_kinds.Domain -> str "domain of "
+     | Some Evar_kinds.Codomain -> str "codomain of ") ++ Evar.print evk
 
 let pr_evar_info evi =
   let open Evd in
@@ -252,7 +267,7 @@ let compute_evar_dependency_graph sigma =
     in
     match evar_body evi with
     | Evar_empty -> acc
-    | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term c) acc
+    | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term (EConstr.Unsafe.to_constr c)) acc
   in
   Evd.fold fold sigma EvMap.empty
 
@@ -290,7 +305,7 @@ let has_no_evar sigma =
   with Exit -> false
 
 let pr_evd_level evd = UState.pr_uctx_level (Evd.evar_universe_context evd)
-let reference_of_level evd l = UState.reference_of_level (Evd.evar_universe_context evd) l
+let reference_of_level evd l = UState.qualid_of_level (Evd.evar_universe_context evd) l
 
 let pr_evar_universe_context ctx =
   let open UState in
@@ -302,7 +317,7 @@ let pr_evar_universe_context ctx =
      str"ALGEBRAIC UNIVERSES:"++brk(0,1)++
      h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++
      str"UNDEFINED UNIVERSES:"++brk(0,1)++
-     h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++
+     h 0 (UnivSubst.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++
      str "WEAK CONSTRAINTS:"++brk(0,1)++
      h 0 (UState.pr_weak prl ctx) ++ fnl ())
 
@@ -310,7 +325,8 @@ let print_env_short env =
   let print_constr = print_kconstr in
   let pr_rel_decl = function
     | RelDecl.LocalAssum (n,_) -> Name.print n
-    | RelDecl.LocalDef (n,b,_) -> str "(" ++ Name.print n ++ str " := " ++ print_constr b ++ str ")"
+    | RelDecl.LocalDef (n,b,_) -> str "(" ++ Name.print n ++ str " := "
+                                  ++ print_constr (EConstr.of_constr b) ++ str ")"
   in
   let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in
   let nc = List.rev (named_context env) in
@@ -331,11 +347,11 @@ let pr_evar_constraints sigma pbs =
       Namegen.make_all_name_different env sigma
     in
     print_env_short env ++ spc () ++ str "|-" ++ spc () ++
-      protect (print_constr_env env sigma) (EConstr.of_constr t1) ++ spc () ++
+      protect (print_constr_env env sigma) t1 ++ spc () ++
       str (match pbty with
             | Reduction.CONV -> "=="
             | Reduction.CUMUL -> "<=") ++
-      spc () ++ protect (print_constr_env env Evd.empty) (EConstr.of_constr t2)
+      spc () ++ protect (print_constr_env env @@ Evd.from_env env) t2
   in
   prlist_with_sep fnl pr_evconstr pbs
 
@@ -429,27 +445,29 @@ let pr_metaset metas =
 
 let pr_var_decl env decl =
   let open NamedDecl in
+  let evd = Evd.from_env env in
   let pbody = match decl with
     | LocalAssum _ ->  mt ()
     | LocalDef (_,c,_) ->
 	(* Force evaluation *)
 	let c = EConstr.of_constr c in
-	let pb = print_constr_env env Evd.empty c in
+        let pb = print_constr_env env evd c in
 	  (str" := " ++ pb ++ cut () ) in
-  let pt = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in
+  let pt = print_constr_env env evd (EConstr.of_constr (get_type decl)) in
   let ptyp = (str" : " ++ pt) in
     (Id.print (get_id decl) ++ hov 0 (pbody ++ ptyp))
 
 let pr_rel_decl env decl =
   let open RelDecl in
+  let evd = Evd.from_env env in
   let pbody = match decl with
     | LocalAssum _ -> mt ()
     | LocalDef (_,c,_) ->
 	(* Force evaluation *)
 	let c = EConstr.of_constr c in
-	let pb = print_constr_env env Evd.empty c in
+        let pb = print_constr_env env evd c in
 	  (str":=" ++ spc () ++ pb ++ spc ()) in
-  let ptyp = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in
+  let ptyp = print_constr_env env evd (EConstr.of_constr (get_type decl)) in
     match get_name decl with
       | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
       | Name id -> hov 0 (Id.print id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
@@ -771,24 +789,23 @@ let map_constr_with_full_binders sigma g f l cstr =
 
 let fold_constr_with_full_binders sigma g f n acc c =
   let open RelDecl in
-  let inj c = EConstr.Unsafe.to_constr c in
   match EConstr.kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> acc
   | Cast (c,_, t) -> f n (f n acc c) t
-  | Prod (na,t,c) -> f (g (LocalAssum (na, inj t)) n) (f n acc t) c
-  | Lambda (na,t,c) -> f (g (LocalAssum (na, inj t)) n) (f n acc t) c
-  | LetIn (na,b,t,c) -> f (g (LocalDef (na, inj b, inj t)) n) (f n (f n acc b) t) c
+  | Prod (na,t,c) -> f (g (LocalAssum (na, t)) n) (f n acc t) c
+  | Lambda (na,t,c) -> f (g (LocalAssum (na, t)) n) (f n acc t) c
+  | LetIn (na,b,t,c) -> f (g (LocalDef (na, b, t)) n) (f n (f n acc b) t) c
   | App (c,l) -> Array.fold_left (f n) (f n acc c) l
   | Proj (p,c) -> f n acc c
   | Evar (_,l) -> Array.fold_left (f n) acc l
   | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
   | Fix (_,(lna,tl,bl)) ->
-      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, inj t)) c) n lna tl in
+      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, t)) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
   | CoFix (_,(lna,tl,bl)) ->
-      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, inj t)) c) n lna tl in
+      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, t)) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
 
@@ -847,6 +864,13 @@ let occur_meta_or_existential sigma c =
     | _ -> EConstr.iter sigma occrec c
   in try occrec c; false with Occur -> true
 
+let occur_metavariable sigma m c =
+  let rec occrec c = match EConstr.kind sigma c with
+  | Meta m' -> if Int.equal m m' then raise Occur
+  | _ -> EConstr.iter sigma occrec c
+  in
+  try occrec c; false with Occur -> true
+
 let occur_evar sigma n c =
   let rec occur_rec c = match EConstr.kind sigma c with
     | Evar (sp,_) when Evar.equal sp n -> raise Occur
@@ -926,7 +950,7 @@ let dependent_main noevar sigma m t =
       match EConstr.kind sigma m, EConstr.kind sigma t with
 	| App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
 	    deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
-	    CArray.Fun1.iter deprec m
+            Array.Fun1.iter deprec m
 	      (Array.sub lt
 		(Array.length lm) ((Array.length lt) - (Array.length lm)))
 	| _, Cast (c,_,_) when noevar && isMeta sigma c -> ()
@@ -964,9 +988,6 @@ let count_occurrences sigma m t =
   countrec m t;
   !n
 
-(* Synonymous *)
-let occur_term = dependent
-
 let pop t = EConstr.Vars.lift (-1) t
 
 (***************************)
@@ -1149,15 +1170,14 @@ let is_template_polymorphic env sigma f =
 
 let base_sort_cmp pb s0 s1 =
   match (s0,s1) with
-    | (Prop c1, Prop c2) -> c1 == Null || c2 == Pos  (* Prop <= Set *)
-    | (Prop c1, Type u)  -> pb == Reduction.CUMUL
-    | (Type u1, Type u2) -> true
-    | _ -> false
+  | Prop, Prop | Set, Set | Type _, Type _ -> true
+  | Prop, Set | Prop, Type _ | Set, Type _ -> pb == Reduction.CUMUL
+  | Set, Prop | Type _, Prop | Type _, Set -> false
 
 let rec is_Prop sigma c = match EConstr.kind sigma c with
   | Sort u ->
     begin match EConstr.ESorts.kind sigma u with
-    | Prop Null -> true
+    | Prop -> true
     | _ -> false
     end
   | Cast (c,_,_) -> is_Prop sigma c
@@ -1166,7 +1186,7 @@ let rec is_Prop sigma c = match EConstr.kind sigma c with
 let rec is_Set sigma c = match EConstr.kind sigma c with
   | Sort u ->
     begin match EConstr.ESorts.kind sigma u with
-    | Prop Pos -> true
+    | Set -> true
     | _ -> false
     end
   | Cast (c,_,_) -> is_Set sigma c
@@ -1369,7 +1389,7 @@ let smash_rel_context sign =
 let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init
 
 let mem_named_context_val id ctxt =
-  try ignore(Environ.lookup_named_val id ctxt); true with Not_found -> false
+  try ignore(Environ.lookup_named_ctxt id ctxt); true with Not_found -> false
 
 let map_rel_decl f = function
 | RelDecl.LocalAssum (id, t) -> RelDecl.LocalAssum (id, f t)
@@ -1495,3 +1515,6 @@ let env_rel_context_chop k env =
   let ctx1,ctx2 = List.chop k rels in
   push_rel_context ctx2 (reset_with_named_context (named_context_val env) env),
   ctx1
+end
+
+include Internal
diff --git a/engine/termops.mli b/engine/termops.mli
index 3b0c4bba..821d9041 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -43,14 +43,14 @@ val it_mkProd : types -> (Name.t * types) list -> types
 val it_mkLambda : constr -> (Name.t * types) list -> constr
 val it_mkProd_or_LetIn : types -> rel_context -> types
 val it_mkProd_wo_LetIn : types -> rel_context -> types
-val it_mkLambda_or_LetIn : Constr.constr -> Context.Rel.t -> Constr.constr
+val it_mkLambda_or_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr
 val it_mkNamedProd_or_LetIn : types -> named_context -> types
-val it_mkNamedProd_wo_LetIn : Constr.types -> Context.Named.t -> Constr.types
+val it_mkNamedProd_wo_LetIn : Constr.types -> Constr.named_context -> Constr.types
 val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr
 
 (* Ad hoc version reinserting letin, assuming the body is defined in
    the context where the letins are expanded *)
-val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Context.Rel.t -> Constr.constr
+val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr
 
 (** {6 Generic iterators on constr} *)
 
@@ -75,8 +75,9 @@ val fold_constr_with_binders : Evd.evar_map ->
   ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
 
 val fold_constr_with_full_binders : Evd.evar_map ->
-  (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) ->
-    'a -> 'b -> constr -> 'b
+  (rel_declaration -> 'a -> 'a) ->
+  ('a -> 'b -> constr -> 'b) ->
+  'a -> 'b -> constr -> 'b
 
 val iter_constr_with_full_binders : Evd.evar_map ->
   (rel_declaration -> 'a -> 'a) ->
@@ -94,6 +95,7 @@ exception Occur
 val occur_meta : Evd.evar_map -> constr -> bool
 val occur_existential : Evd.evar_map -> constr -> bool
 val occur_meta_or_existential : Evd.evar_map -> constr -> bool
+val occur_metavariable : Evd.evar_map -> metavariable -> constr -> bool
 val occur_evar : Evd.evar_map -> Evar.t -> constr -> bool
 val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool
 val occur_var_in_decl :
@@ -112,9 +114,7 @@ val dependent_in_decl : Evd.evar_map -> constr -> named_declaration -> bool
 val count_occurrences : Evd.evar_map -> constr -> constr -> int
 val collect_metas : Evd.evar_map -> constr -> int list
 val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *)
-val vars_of_global_reference : env -> Globnames.global_reference -> Id.Set.t
-val occur_term : Evd.evar_map -> constr -> constr -> bool (** Synonymous of dependent *)
-[@@ocaml.deprecated "alias of Termops.dependent"]
+val vars_of_global_reference : env -> GlobRef.t -> Id.Set.t
 
 (* Substitution of metavariables *)
 type meta_value_map = (metavariable * Constr.constr) list
@@ -225,7 +225,7 @@ val names_of_rel_context : env -> names_context
 (* [context_chop n Γ] returns (Γ₁,Γ₂) such that [Γ]=[Γ₂Γ₁], [Γ₁] has
    [n] hypotheses, excluding local definitions, and [Γ₁], if not empty,
    starts with an hypothesis (i.e. [Γ₁] has the form empty or [x:A;Γ₁'] *)
-val context_chop : int -> Context.Rel.t -> Context.Rel.t * Context.Rel.t
+val context_chop : int -> Constr.rel_context -> Constr.rel_context * Constr.rel_context
 
 (* [env_rel_context_chop n env] extracts out the [n] top declarations
    of the rel_context part of [env], counting both local definitions and
@@ -239,19 +239,19 @@ val add_vname : Id.Set.t -> Name.t -> Id.Set.t
 (** other signature iterators *)
 val process_rel_context : (rel_declaration -> env -> env) -> env -> env
 val assums_of_rel_context : ('c, 't) Context.Rel.pt -> (Name.t * 't) list
-val lift_rel_context : int -> Context.Rel.t -> Context.Rel.t
-val substl_rel_context : Constr.constr list -> Context.Rel.t -> Context.Rel.t
-val smash_rel_context : Context.Rel.t -> Context.Rel.t (** expand lets in context *)
+val lift_rel_context : int -> Constr.rel_context -> Constr.rel_context
+val substl_rel_context : Constr.constr list -> Constr.rel_context -> Constr.rel_context
+val smash_rel_context : Constr.rel_context -> Constr.rel_context (** expand lets in context *)
 
 val map_rel_context_in_env :
-  (env -> Constr.constr -> Constr.constr) -> env -> Context.Rel.t -> Context.Rel.t
+  (env -> Constr.constr -> Constr.constr) -> env -> Constr.rel_context -> Constr.rel_context
 val map_rel_context_with_binders :
   (int -> 'c -> 'c) -> ('c, 'c) Context.Rel.pt -> ('c, 'c) Context.Rel.pt
 val fold_named_context_both_sides :
-  ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) ->
-    Context.Named.t -> init:'a -> 'a
+  ('a -> Constr.named_declaration -> Constr.named_declaration list -> 'a) ->
+    Constr.named_context -> init:'a -> 'a
 val mem_named_context_val : Id.t -> named_context_val -> bool
-val compact_named_context : Context.Named.t -> Context.Compacted.t
+val compact_named_context : Constr.named_context -> Constr.compacted_context
 
 val map_rel_decl : ('a -> 'b) -> ('a, 'a) Context.Rel.Declaration.pt -> ('b, 'b) Context.Rel.Declaration.pt
 val map_named_decl : ('a -> 'b) -> ('a, 'a) Context.Named.Declaration.pt -> ('b, 'b) Context.Named.Declaration.pt
@@ -261,7 +261,7 @@ val clear_named_body : Id.t -> env -> env
 val global_vars : env -> Evd.evar_map -> constr -> Id.t list
 val global_vars_set : env -> Evd.evar_map -> constr -> Id.Set.t
 val global_vars_set_of_decl : env -> Evd.evar_map -> named_declaration -> Id.Set.t
-val global_app_of_constr : Evd.evar_map -> constr -> (Globnames.global_reference * EInstance.t) * constr option
+val global_app_of_constr : Evd.evar_map -> constr -> (GlobRef.t * EInstance.t) * constr option
 
 (** Gives an ordered list of hypotheses, closed by dependencies,
    containing a given set *)
@@ -270,9 +270,9 @@ val dependency_closure : env -> Evd.evar_map -> named_context -> Id.Set.t -> Id.
 (** Test if an identifier is the basename of a global reference *)
 val is_section_variable : Id.t -> bool
 
-val global_of_constr : Evd.evar_map -> constr -> Globnames.global_reference * EInstance.t
+val global_of_constr : Evd.evar_map -> constr -> GlobRef.t * EInstance.t
 
-val is_global : Evd.evar_map -> Globnames.global_reference -> constr -> bool
+val is_global : Evd.evar_map -> GlobRef.t -> constr -> bool
 
 val isGlobalRef : Evd.evar_map -> constr -> bool
 
@@ -282,7 +282,7 @@ val is_Prop : Evd.evar_map -> constr -> bool
 val is_Set : Evd.evar_map -> constr -> bool
 val is_Type : Evd.evar_map -> constr -> bool
 
-val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.reference
+val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid
 
 (** Combinators on judgments *)
 
@@ -307,12 +307,40 @@ val pr_metaset : Metaset.t -> Pp.t
 val pr_evar_universe_context : UState.t -> Pp.t
 val pr_evd_level : evar_map -> Univ.Level.t -> Pp.t
 
-(** debug printer: do not use to display terms to the casual user... *)
+module Internal : sig
 
-val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit
-val print_constr     : constr -> Pp.t
+(** NOTE: to print terms you always want to use functions in
+   Printer, not these ones which are for very special cases. *)
+
+(** debug printers: print raw form for terms, both with
+   evar-substitution and without.  *)
+val debug_print_constr : constr -> Pp.t
+val debug_print_constr_env : env -> evar_map -> constr -> Pp.t
+
+(** Pretty-printer hook: [print_constr_env env sigma c] will pretty
+   print c if the pretty printing layer has been linked into the Coq
+   binary. *)
 val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t
+
+(** [set_print_constr f] sets f to be the pretty printer *)
+val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit
+
+(** Printers for contexts *)
 val print_named_context : env -> Pp.t
-val pr_rel_decl : env -> Context.Rel.Declaration.t -> Pp.t
+val pr_rel_decl : env -> Constr.rel_declaration -> Pp.t
 val print_rel_context : env -> Pp.t
 val print_env : env -> Pp.t
+
+val print_constr : constr -> Pp.t
+[@@deprecated "use print_constr_env"]
+
+end
+
+val print_constr : constr -> Pp.t
+[@@deprecated "This is an internal, debug printer. WARNING, it is *extremely* likely that you want to use [Printer.pr_econstr_env] instead"]
+
+val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t
+[@@deprecated "This is an internal, debug printer. WARNING, it is *extremely* likely that you want to use [Printer.pr_econstr_env] instead"]
+
+val print_rel_context : env -> Pp.t
+[@@deprecated "This is an internal, debug printer. WARNING, this function is not suitable for plugin code, if you still want to use it then call [Internal.print_rel_context] instead"]
diff --git a/engine/uState.ml b/engine/uState.ml
index 6c8dbe3f..29cb3c9b 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -20,14 +20,14 @@ type uinfo = {
   uloc : Loc.t option;
 }
 
-module UPairSet = Universes.UPairSet
+module UPairSet = UnivMinim.UPairSet
 
 (* 2nd part used to check consistency on the fly. *)
 type t =
- { uctx_names : Universes.universe_binders * uinfo Univ.LMap.t;
+ { uctx_names : UnivNames.universe_binders * uinfo Univ.LMap.t;
    uctx_local : Univ.ContextSet.t; (** The local context of variables *)
    uctx_seff_univs : Univ.LSet.t; (** Local universes used through private constants *)
-   uctx_univ_variables : Universes.universe_opt_subst;
+   uctx_univ_variables : UnivSubst.universe_opt_subst;
    (** The local universes that are unification variables *)
    uctx_univ_algebraic : Univ.LSet.t; 
    (** The subset of unification variables that can be instantiated with
@@ -152,11 +152,12 @@ let drop_weak_constraints = ref false
 
 let process_universe_constraints ctx cstrs =
   let open Univ in
-  let open Universes in
+  let open UnivSubst in
+  let open UnivProblem in
   let univs = ctx.uctx_universes in
   let vars = ref ctx.uctx_univ_variables in
   let weak = ref ctx.uctx_weak_constraints in
-  let normalize = normalize_univ_variable_opt_subst vars in
+  let normalize u = normalize_univ_variable_opt_subst !vars u in
   let nf_constraint = function
     | ULub (u, v) -> ULub (level_subst_of normalize u, level_subst_of normalize v)
     | UWeak (u, v) -> UWeak (level_subst_of normalize u, level_subst_of normalize v)
@@ -203,7 +204,7 @@ let process_universe_constraints ctx cstrs =
   in
   let unify_universes cst local =
     let cst = nf_constraint cst in
-      if Constraints.is_trivial cst then local
+      if UnivProblem.is_trivial cst then local
       else 
           match cst with
           | ULe (l, r) ->
@@ -241,7 +242,7 @@ let process_universe_constraints ctx cstrs =
           | UEq (l, r) -> equalize_universes l r local
   in
   let local = 
-    Constraints.fold unify_universes cstrs Univ.Constraint.empty
+    UnivProblem.Set.fold unify_universes cstrs Univ.Constraint.empty
   in
     !vars, !weak, local
 
@@ -249,13 +250,14 @@ let add_constraints 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' = match d with
+    let cstr' = let open UnivProblem in
+      match d with
       | Univ.Lt ->
-        Universes.ULe (Univ.Universe.super l, r)
-      | Univ.Le -> Universes.ULe (l, r)
-      | Univ.Eq -> Universes.UEq (l, r)
-    in Universes.Constraints.add cstr' acc)
-    cstrs Universes.Constraints.empty
+        ULe (Univ.Universe.super l, r)
+      | Univ.Le -> ULe (l, r)
+      | Univ.Eq -> UEq (l, r)
+    in UnivProblem.Set.add cstr' acc)
+    cstrs UnivProblem.Set.empty
   in
   let vars, weak, local' = process_universe_constraints ctx cstrs' in
   { ctx with
@@ -293,18 +295,30 @@ let constrain_variables diff ctx =
   in
   { ctx with uctx_local = (univs, local); uctx_univ_variables = vars }
   
-let reference_of_level uctx =
+let qualid_of_level uctx =
   let map, map_rev = uctx.uctx_names in 
     fun l ->
-      try CAst.make @@ Libnames.Ident (Option.get (Univ.LMap.find l map_rev).uname)
+      try Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname)
       with Not_found | Option.IsNone ->
-        Universes.reference_of_level l
+        UnivNames.qualid_of_level l
 
 let pr_uctx_level uctx l =
-  Libnames.pr_reference (reference_of_level uctx l)
+  Libnames.pr_qualid (qualid_of_level uctx l)
+
+type ('a, 'b) gen_universe_decl = {
+  univdecl_instance : 'a; (* Declared universes *)
+  univdecl_extensible_instance : bool; (* Can new universes be added *)
+  univdecl_constraints : 'b; (* Declared constraints *)
+  univdecl_extensible_constraints : bool (* Can new constraints be added *) }
 
 type universe_decl =
-  (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
+  (lident list, Univ.Constraint.t) gen_universe_decl
+
+let default_univ_decl =
+  { univdecl_instance = [];
+    univdecl_extensible_instance = true;
+    univdecl_constraints = Univ.Constraint.empty;
+    univdecl_extensible_constraints = true }
 
 let error_unbound_universes left uctx =
   let open Univ in
@@ -365,7 +379,6 @@ let check_implication uctx cstrs cstrs' =
       (str "Universe constraints are not implied by the ones declared.")
 
 let check_mono_univ_decl uctx decl =
-  let open Misctypes in
   let () =
     let names = decl.univdecl_instance in
     let extensible = decl.univdecl_extensible_instance in
@@ -378,7 +391,6 @@ let check_mono_univ_decl uctx decl =
   uctx.uctx_local
 
 let check_univ_decl ~poly uctx decl =
-  let open Misctypes in
   let ctx =
     let names = decl.univdecl_instance in
     let extensible = decl.univdecl_extensible_instance in
@@ -418,10 +430,17 @@ let univ_rigid = UnivRigid
 let univ_flexible = UnivFlexible false
 let univ_flexible_alg = UnivFlexible true
 
-let merge ?loc sideff rigid uctx ctx' =
+(** ~sideff indicates that it is ok to redeclare a universe.
+    ~extend also merges the universe context in the local constraint structures
+    and not only in the graph. This depends if the
+    context we merge comes from a side effect that is already inlined
+    or defined separately. In the later case, there is no extension,
+    see [emit_side_effects] for example. *)
+let merge ?loc ~sideff ~extend rigid uctx ctx' =
   let open Univ in
   let levels = ContextSet.levels ctx' in
-  let uctx = if sideff then uctx else
+  let uctx =
+    if not extend then uctx else
     match rigid with
     | UnivRigid -> uctx
     | UnivFlexible b ->
@@ -436,9 +455,8 @@ let merge ?loc sideff rigid uctx ctx' =
         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
+    if not extend 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
@@ -467,11 +485,11 @@ let merge_subst uctx s =
 
 let emit_side_effects eff u =
   let uctxs = Safe_typing.universes_of_private eff in
-  List.fold_left (merge true univ_rigid) u uctxs
+  List.fold_left (merge ~sideff:true ~extend:false univ_rigid) u uctxs
 
 let new_univ_variable ?loc rigid name
   ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
-  let u = Universes.new_univ_level () in
+  let u = UnivGen.new_univ_level () in
   let ctx' = Univ.ContextSet.add_universe u ctx in
   let uctx', pred =
     match rigid with
@@ -549,14 +567,33 @@ let is_sort_variable uctx s =
   | _ -> None
 
 let subst_univs_context_with_def def usubst (ctx, cst) =
-  (Univ.LSet.diff ctx def, Universes.subst_univs_constraints usubst cst)
+  (Univ.LSet.diff ctx def, UnivSubst.subst_univs_constraints usubst cst)
+
+let is_trivial_leq (l,d,r) =
+  Univ.Level.is_prop l && (d == Univ.Le || (d == Univ.Lt && Univ.Level.is_set r))
+
+(* Prop < i <-> Set+1 <= i <-> Set < i *)
+let translate_cstr (l,d,r as cstr) =
+  let open Univ in
+  if Level.equal Level.prop l && d == Univ.Lt && not (Level.equal Level.set r) then
+    (Level.set, d, r)
+  else cstr
+
+let refresh_constraints univs (ctx, cstrs) =
+  let cstrs', univs' =
+    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', UGraph.enforce_constraint c univs))
+      cstrs (Univ.Constraint.empty, univs)
+  in ((ctx, cstrs'), univs')
 
 let normalize_variables uctx =
-  let normalized_variables, undef, def, subst = 
-    Universes.normalize_univ_variables uctx.uctx_univ_variables 
+  let normalized_variables, def, subst =
+    UnivSubst.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
+  let ctx_local', univs = refresh_constraints uctx.uctx_initial_universes ctx_local in
     subst, { uctx with uctx_local = ctx_local';
       uctx_univ_variables = normalized_variables;
       uctx_universes = univs }
@@ -582,7 +619,7 @@ let fix_undefined_variables uctx =
     uctx_univ_algebraic = algs' }
 
 let refresh_undefined_univ_variables uctx =
-  let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in
+  let subst, ctx' = UnivGen.fresh_universe_context_set_instance uctx.uctx_local in
   let subst_fn u = Univ.subst_univs_level_level subst u in
   let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (subst_fn u) acc)
     uctx.uctx_univ_algebraic Univ.LSet.empty 
@@ -609,7 +646,7 @@ let refresh_undefined_univ_variables uctx =
     uctx', subst
 
 let minimize uctx =
-  let open Universes in
+  let open UnivMinim in
   let ((vars',algs'), us') =
     normalize_context_set uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables
       uctx.uctx_univ_algebraic uctx.uctx_weak_constraints
@@ -637,11 +674,8 @@ let update_sigma_env uctx env =
     { uctx with uctx_initial_universes = univs;
                          uctx_universes = univs }
   in
-  merge true univ_rigid eunivs eunivs.uctx_local
+  merge ~sideff:true ~extend:false univ_rigid eunivs eunivs.uctx_local
 
 let pr_weak prl {uctx_weak_constraints=weak} =
   let open Pp in
   prlist_with_sep fnl (fun (u,v) -> prl u ++ str " ~ " ++ prl v) (UPairSet.elements weak)
-
-(** Deprecated *)
-let normalize = minimize
diff --git a/engine/uState.mli b/engine/uState.mli
index 48c38faf..f833508e 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -26,7 +26,7 @@ val empty : t
 
 val make : UGraph.t -> t
 
-val make_with_initial_binders : UGraph.t -> Misctypes.lident list -> t
+val make_with_initial_binders : UGraph.t -> lident list -> t
 
 val is_empty : t -> bool
 
@@ -34,9 +34,9 @@ val union : t -> t -> t
 
 val of_context_set : Univ.ContextSet.t -> t
 
-val of_binders : Universes.universe_binders -> t
+val of_binders : UnivNames.universe_binders -> t
 
-val universe_binders : t -> Universes.universe_binders
+val universe_binders : t -> UnivNames.universe_binders
 
 (** {5 Projections} *)
 
@@ -44,7 +44,7 @@ val context_set : t -> Univ.ContextSet.t
 (** The local context of the state, i.e. a set of bound variables together
     with their associated constraints. *)
 
-val subst : t -> Universes.universe_opt_subst
+val subst : t -> UnivSubst.universe_opt_subst
 (** The local universes that are unification variables *)
 
 val ugraph : t -> UGraph.t
@@ -79,7 +79,7 @@ val add_constraints : t -> Univ.Constraint.t -> t
   @raise UniversesDiffer when universes differ
 *)
 
-val add_universe_constraints : t -> Universes.Constraints.t -> t
+val add_universe_constraints : t -> UnivProblem.Set.t -> t
 (**
   @raise UniversesDiffer when universes differ
 *)
@@ -103,8 +103,8 @@ val univ_rigid : rigid
 val univ_flexible : rigid
 val univ_flexible_alg : rigid
 
-val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.ContextSet.t -> t
-val merge_subst : t -> Universes.universe_opt_subst -> t
+val merge : ?loc:Loc.t -> sideff:bool -> extend:bool -> rigid -> t -> Univ.ContextSet.t -> t
+val merge_subst : t -> UnivSubst.universe_opt_subst -> t
 val emit_side_effects : Safe_typing.private_constants -> t -> t
 
 val new_univ_variable : ?loc:Loc.t -> rigid -> Id.t option -> t -> t * Univ.Level.t
@@ -137,11 +137,17 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
 
 (** Universe minimization *)
 val minimize : t -> t
-val normalize : t -> t
-[@@ocaml.deprecated "Alias of UState.minimize"]
+
+type ('a, 'b) gen_universe_decl = {
+  univdecl_instance : 'a; (* Declared universes *)
+  univdecl_extensible_instance : bool; (* Can new universes be added *)
+  univdecl_constraints : 'b; (* Declared constraints *)
+  univdecl_extensible_constraints : bool (* Can new constraints be added *) }
 
 type universe_decl =
-  (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
+  (lident list, Univ.Constraint.t) gen_universe_decl
+
+val default_univ_decl : universe_decl
 
 (** [check_univ_decl ctx decl]
 
@@ -165,6 +171,6 @@ val update_sigma_env : t -> Environ.env -> t
 (** {5 Pretty-printing} *)
 
 val pr_uctx_level : t -> Univ.Level.t -> Pp.t
-val reference_of_level : t -> Univ.Level.t -> Libnames.reference
+val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid
 
 val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t
diff --git a/engine/univGen.ml b/engine/univGen.ml
new file mode 100644
index 00000000..b07d4848
--- /dev/null
+++ b/engine/univGen.ml
@@ -0,0 +1,246 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Sorts
+open Names
+open Constr
+open Environ
+open Univ
+
+(* Generator of levels *)
+type universe_id = DirPath.t * int
+
+let new_univ_id, set_remote_new_univ_id =
+  RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1)
+    ~build:(fun n -> Global.current_dirpath (), n)
+
+let new_univ_level () =
+  let dp, id = new_univ_id () in
+  Univ.Level.make dp id
+
+let fresh_level () = new_univ_level ()
+
+(* TODO: remove *)
+let new_univ dp = Univ.Universe.make (new_univ_level dp)
+let new_Type dp = mkType (new_univ dp)
+let new_Type_sort dp = Type (new_univ dp)
+
+let fresh_universe_instance ctx =
+  let init _ = new_univ_level () in
+  Instance.of_array (Array.init (AUContext.size ctx) init)
+
+let fresh_instance_from_context ctx =
+  let inst = fresh_universe_instance ctx in
+  let constraints = AUContext.instantiate inst ctx in
+    inst, constraints
+
+let fresh_instance ctx =
+  let ctx' = ref LSet.empty in
+  let init _ =
+    let u = new_univ_level () in
+    ctx' := LSet.add u !ctx'; u
+  in
+  let inst = Instance.of_array (Array.init (AUContext.size ctx) init)
+  in !ctx', inst
+
+let existing_instance ctx inst =
+  let () =
+    let len1 = Array.length (Instance.to_array inst)
+    and len2 = AUContext.size ctx in
+      if not (len1 == len2) then
+        CErrors.user_err ~hdr:"Universes"
+          Pp.(str "Polymorphic constant expected " ++ int len2 ++
+              str" levels but was given " ++ int len1)
+      else ()
+  in LSet.empty, inst
+
+let fresh_instance_from ctx inst =
+  let ctx', inst =
+    match inst with
+    | Some inst -> existing_instance ctx inst
+    | None -> fresh_instance ctx
+  in
+  let constraints = AUContext.instantiate inst ctx in
+    inst, (ctx', constraints)
+
+(** Fresh universe polymorphic construction *)
+
+let fresh_constant_instance env c inst =
+  let cb = lookup_constant c env in
+  match cb.Declarations.const_universes with
+  | Declarations.Monomorphic_const _ -> ((c,Instance.empty), ContextSet.empty)
+  | Declarations.Polymorphic_const auctx ->
+    let inst, ctx =
+      fresh_instance_from auctx inst
+    in
+    ((c, inst), ctx)
+
+let fresh_inductive_instance env ind inst =
+  let mib, mip = Inductive.lookup_mind_specif env ind in
+  match mib.Declarations.mind_universes with
+  | Declarations.Monomorphic_ind _ ->
+    ((ind,Instance.empty), ContextSet.empty)
+  | Declarations.Polymorphic_ind uactx ->
+    let inst, ctx = (fresh_instance_from uactx) inst in
+     ((ind,inst), ctx)
+  | Declarations.Cumulative_ind acumi ->
+    let inst, ctx =
+      fresh_instance_from (Univ.ACumulativityInfo.univ_context acumi) inst
+    in ((ind,inst), ctx)
+
+let fresh_constructor_instance env (ind,i) inst =
+  let mib, mip = Inductive.lookup_mind_specif env ind in
+  match mib.Declarations.mind_universes with
+  | Declarations.Monomorphic_ind _ -> (((ind,i),Instance.empty), ContextSet.empty)
+  | Declarations.Polymorphic_ind auctx ->
+    let inst, ctx = fresh_instance_from auctx  inst in
+        (((ind,i),inst), ctx)
+  | Declarations.Cumulative_ind acumi ->
+    let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in
+    (((ind,i),inst), ctx)
+
+open Globnames
+
+let fresh_global_instance ?names env gr =
+  match gr with
+  | VarRef id -> mkVar id, ContextSet.empty
+  | ConstRef sp ->
+     let c, ctx = fresh_constant_instance env sp names in
+       mkConstU c, ctx
+  | ConstructRef sp ->
+     let c, ctx = fresh_constructor_instance env sp names in
+       mkConstructU c, ctx
+  | IndRef sp ->
+     let c, ctx = fresh_inductive_instance env sp names in
+       mkIndU c, ctx
+
+let fresh_constant_instance env sp =
+  fresh_constant_instance env sp None
+
+let fresh_inductive_instance env sp =
+  fresh_inductive_instance env sp None
+
+let fresh_constructor_instance env sp =
+  fresh_constructor_instance env sp None
+
+let constr_of_global gr =
+  let c, ctx = fresh_global_instance (Global.env ()) gr in
+    if not (Univ.ContextSet.is_empty ctx) then
+      if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then
+        (* Should be an error as we might forget constraints, allow for now
+           to make firstorder work with "using" clauses *)
+        c
+      else CErrors.user_err ~hdr:"constr_of_global"
+          Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
+              str " would forget universes.")
+    else c
+
+let constr_of_global_univ (gr,u) =
+  match gr with
+  | VarRef id -> mkVar id
+  | ConstRef sp -> mkConstU (sp,u)
+  | ConstructRef sp -> mkConstructU (sp,u)
+  | IndRef sp -> mkIndU (sp,u)
+
+let fresh_global_or_constr_instance env = function
+  | IsConstr c -> c, ContextSet.empty
+  | IsGlobal gr -> fresh_global_instance env gr
+
+let global_of_constr c =
+  match kind c with
+  | Const (c, u) -> ConstRef c, u
+  | Ind (i, u) -> IndRef i, u
+  | Construct (c, u) -> ConstructRef c, u
+  | Var id -> VarRef id, Instance.empty
+  | _ -> raise Not_found
+
+open Declarations
+
+let type_of_reference env r =
+  match r with
+  | VarRef id -> Environ.named_type id env, ContextSet.empty
+  | ConstRef c ->
+     let cb = Environ.lookup_constant c env in
+     let ty = cb.const_type in
+     begin
+       match cb.const_universes with
+       | Monomorphic_const _ -> ty, ContextSet.empty
+       | Polymorphic_const auctx ->
+         let inst, ctx = fresh_instance_from auctx None in
+         Vars.subst_instance_constr inst ty, ctx
+     end
+  | IndRef ind ->
+     let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
+     begin
+       match mib.mind_universes with
+       | Monomorphic_ind _ ->
+         let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in
+         ty, ContextSet.empty
+       | Polymorphic_ind auctx ->
+         let inst, ctx = fresh_instance_from auctx  None in
+         let ty = Inductive.type_of_inductive env (specif, inst) in
+         ty, ctx
+       | Cumulative_ind cumi ->
+         let inst, ctx =
+           fresh_instance_from (ACumulativityInfo.univ_context cumi) None
+         in
+         let ty = Inductive.type_of_inductive env (specif, inst) in
+         ty, ctx
+     end
+
+  | ConstructRef cstr ->
+    let (mib,oib as specif) =
+      Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
+    in
+    begin
+       match mib.mind_universes with
+       | Monomorphic_ind _ ->
+         Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty
+       | Polymorphic_ind auctx ->
+         let inst, ctx = fresh_instance_from auctx None in
+         Inductive.type_of_constructor (cstr,inst) specif, ctx
+       | Cumulative_ind cumi ->
+         let inst, ctx =
+           fresh_instance_from (ACumulativityInfo.univ_context cumi) None
+         in
+         Inductive.type_of_constructor (cstr,inst) specif, ctx
+     end
+
+let type_of_global t = type_of_reference (Global.env ()) t
+
+let fresh_sort_in_family = function
+  | InProp -> Sorts.prop, ContextSet.empty
+  | InSet -> Sorts.set, ContextSet.empty
+  | InType ->
+    let u = fresh_level () in
+      Type (Univ.Universe.make u), ContextSet.singleton u
+
+let new_sort_in_family sf =
+  fst (fresh_sort_in_family sf)
+
+let extend_context (a, ctx) (ctx') =
+  (a, ContextSet.union ctx ctx')
+
+let new_global_univ () =
+  let u = fresh_level () in
+  (Univ.Universe.make u, ContextSet.singleton u)
+
+let fresh_universe_context_set_instance ctx =
+  if ContextSet.is_empty ctx then LMap.empty, ctx
+  else
+    let (univs, cst) = ContextSet.levels ctx, ContextSet.constraints ctx in
+    let univs',subst = LSet.fold
+      (fun u (univs',subst) ->
+        let u' = fresh_level () in
+          (LSet.add u' univs', LMap.add u u' subst))
+      univs (LSet.empty, LMap.empty)
+    in
+    let cst' = subst_univs_level_constraints subst cst in
+      subst, (univs', cst')
diff --git a/engine/univGen.mli b/engine/univGen.mli
new file mode 100644
index 00000000..43942493
--- /dev/null
+++ b/engine/univGen.mli
@@ -0,0 +1,80 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+open Constr
+open Environ
+open Univ
+
+
+(** The global universe counter *)
+type universe_id = DirPath.t * int
+
+val set_remote_new_univ_id : universe_id RemoteCounter.installer
+
+(** Side-effecting functions creating new universe levels. *)
+
+val new_univ_id : unit -> universe_id
+val new_univ_level : unit -> Level.t
+val new_univ : unit -> Universe.t
+val new_Type : unit -> types
+val new_Type_sort : unit -> Sorts.t
+
+val new_global_univ : unit -> Universe.t in_universe_context_set
+val new_sort_in_family : Sorts.family -> Sorts.t
+
+(** Build a fresh instance for a given context, its associated substitution and
+    the instantiated constraints. *)
+
+val fresh_instance_from_context : AUContext.t ->
+  Instance.t constrained
+
+val fresh_instance_from : AUContext.t -> Instance.t option ->
+  Instance.t in_universe_context_set
+
+val fresh_sort_in_family : Sorts.family ->
+  Sorts.t in_universe_context_set
+val fresh_constant_instance : env -> Constant.t ->
+  pconstant in_universe_context_set
+val fresh_inductive_instance : env -> inductive ->
+  pinductive in_universe_context_set
+val fresh_constructor_instance : env -> constructor ->
+  pconstructor in_universe_context_set
+
+val fresh_global_instance : ?names:Univ.Instance.t -> env -> GlobRef.t ->
+  constr in_universe_context_set
+
+val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr ->
+  constr in_universe_context_set
+
+(** Get fresh variables for the universe context.
+    Useful to make tactics that manipulate constrs in universe contexts polymorphic. *)
+val fresh_universe_context_set_instance : ContextSet.t ->
+  universe_level_subst * ContextSet.t
+
+(** Raises [Not_found] if not a global reference. *)
+val global_of_constr : constr -> GlobRef.t puniverses
+
+val constr_of_global_univ : GlobRef.t puniverses -> constr
+
+val extend_context : 'a in_universe_context_set -> ContextSet.t ->
+  'a in_universe_context_set
+
+(** Create a fresh global in the global environment, without side effects.
+    BEWARE: this raises an ANOMALY on polymorphic constants/inductives:
+    the constraints should be properly added to an evd.
+    See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for
+    the proper way to get a fresh copy of a global reference. *)
+val constr_of_global : GlobRef.t -> constr
+
+(** Returns the type of the global reference, by creating a fresh instance of polymorphic
+    references and computing their instantiated universe context. (side-effect on the
+    universe counter, use with care). *)
+val type_of_global : GlobRef.t -> types in_universe_context_set
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
new file mode 100644
index 00000000..f10e6d2e
--- /dev/null
+++ b/engine/univMinim.ml
@@ -0,0 +1,383 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Univ
+open UnivSubst
+
+(* To disallow minimization to Set *)
+let set_minimization = ref true
+let is_set_minimization () = !set_minimization
+
+let _ =
+  Goptions.(declare_bool_option
+          { optdepr  = false;
+            optname  = "minimization to Set";
+            optkey   = ["Universe";"Minimization";"ToSet"];
+            optread  = is_set_minimization;
+            optwrite = (:=) set_minimization })
+
+
+(** Simplification *)
+
+let add_list_map u t map =
+  try
+    let l = LMap.find u map in
+    LMap.set u (t :: l) map
+  with Not_found ->
+    LMap.add u [t] map
+
+(** Precondition: flexible <= ctx *)
+let choose_canonical ctx flexible algs s =
+  let global = LSet.diff s ctx in
+  let flexible, rigid = LSet.partition flexible (LSet.inter s ctx) in
+    (** If there is a global universe in the set, choose it *)
+    if not (LSet.is_empty global) then
+      let canon = LSet.choose global in
+        canon, (LSet.remove canon global, rigid, flexible)
+    else (** No global in the equivalence class, choose a rigid one *)
+        if not (LSet.is_empty rigid) then
+          let canon = LSet.choose rigid in
+            canon, (global, LSet.remove canon rigid, flexible)
+        else (** There are only flexible universes in the equivalence
+                 class, choose a non-algebraic. *)
+          let algs, nonalgs = LSet.partition (fun x -> LSet.mem x algs) flexible in
+            if not (LSet.is_empty nonalgs) then
+              let canon = LSet.choose nonalgs in
+                canon, (global, rigid, LSet.remove canon flexible)
+            else
+              let canon = LSet.choose algs in
+                canon, (global, rigid, LSet.remove canon flexible)
+
+(* Eq < Le < Lt *)
+let compare_constraint_type d d' =
+  match d, d' with
+  | Eq, Eq -> 0
+  | Eq, _ -> -1
+  | _, Eq -> 1
+  | Le, Le -> 0
+  | Le, _ -> -1
+  | _, Le -> 1
+  | Lt, Lt -> 0
+
+type lowermap = constraint_type LMap.t
+
+let lower_union =
+  let merge k a b =
+    match a, b with
+    | Some _, None -> a
+    | None, Some _ -> b
+    | None, None -> None
+    | Some l, Some r ->
+       if compare_constraint_type l r >= 0 then a
+       else b
+  in LMap.merge merge
+
+let lower_add l c m =
+  try let c' = LMap.find l m in
+      if compare_constraint_type c c' > 0 then
+        LMap.add l c m
+      else m
+  with Not_found -> LMap.add l c m
+
+let lower_of_list l =
+  List.fold_left (fun acc (d,l) -> LMap.add l d acc) LMap.empty l
+
+type lbound = { enforce : bool; alg : bool; lbound: Universe.t; lower : lowermap }
+
+exception Found of Level.t * lowermap
+let find_inst insts v =
+  try LMap.iter (fun k {enforce;alg;lbound=v';lower} ->
+    if not alg && enforce && Universe.equal v' v then raise (Found (k, lower)))
+        insts; raise Not_found
+  with Found (f,l) -> (f,l)
+
+let compute_lbound left =
+ (** The universe variable was not fixed yet.
+     Compute its level using its lower bound. *)
+  let sup l lbound =
+    match lbound with
+    | None -> Some l
+    | Some l' -> Some (Universe.sup l l')
+  in
+    List.fold_left (fun lbound (d, l) ->
+      if d == Le (* l <= ?u *) then sup l lbound
+      else (* l < ?u *)
+        (assert (d == Lt);
+         if not (Universe.level l == None) then
+           sup (Universe.super l) lbound
+         else None))
+      None left
+
+let instantiate_with_lbound u lbound lower ~alg ~enforce (ctx, us, algs, insts, cstrs) =
+  if enforce then
+    let inst = Universe.make u in
+    let cstrs' = enforce_leq lbound inst cstrs in
+      (ctx, us, LSet.remove u algs,
+       LMap.add u {enforce;alg;lbound;lower} insts, cstrs'),
+      {enforce; alg; lbound=inst; lower}
+  else (* Actually instantiate *)
+    (Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs,
+     LMap.add u {enforce;alg;lbound;lower} insts, cstrs),
+    {enforce; alg; lbound; lower}
+
+type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t
+
+let _pr_constraints_map (cmap:constraints_map) =
+  let open Pp in
+  LMap.fold (fun l cstrs acc ->
+    Level.pr l ++ str " => " ++
+      prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++
+      fnl () ++ acc)
+    cmap (mt ())
+
+let remove_alg l (ctx, us, algs, insts, cstrs) =
+  (ctx, us, LSet.remove l algs, insts, cstrs)
+
+let not_lower lower (d,l) =
+  (* We're checking if (d,l) is already implied by the lower
+     constraints on some level u. If it represents l < u (d is Lt
+     or d is Le and i > 0, the i < 0 case is impossible due to
+     invariants of Univ), and the lower constraints only have l <=
+     u then it is not implied. *)
+  Univ.Universe.exists
+    (fun (l,i) ->
+       let d =
+         if i == 0 then d
+         else match d with
+           | Le -> Lt
+           | d -> d
+       in
+       try let d' = LMap.find l lower in
+         (* If d is stronger than the already implied lower
+          * constraints we must keep it. *)
+         compare_constraint_type d d' > 0
+       with Not_found ->
+         (** No constraint existing on l *) true) l
+
+exception UpperBoundedAlg
+(** [enforce_uppers upper lbound cstrs] interprets [upper] as upper
+   constraints to [lbound], adding them to [cstrs].
+
+    @raise UpperBoundedAlg if any [upper] constraints are strict and
+   [lbound] algebraic. *)
+let enforce_uppers upper lbound cstrs =
+  List.fold_left (fun cstrs (d, r) ->
+      if d == Univ.Le then
+        enforce_leq lbound (Universe.make r) cstrs
+      else
+        match Universe.level lbound with
+        | Some lev -> Constraint.add (lev, d, r) cstrs
+        | None -> raise UpperBoundedAlg)
+    cstrs upper
+
+let minimize_univ_variables ctx us algs left right cstrs =
+  let left, lbounds =
+    Univ.LMap.fold (fun r lower (left, lbounds as acc)  ->
+      if Univ.LMap.mem r us || not (Univ.LSet.mem r ctx) then acc
+      else (* Fixed universe, just compute its glb for sharing *)
+        let lbounds =
+          match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with
+          | None -> lbounds
+          | Some lbound -> LMap.add r {enforce=true; alg=false; lbound; lower=lower_of_list lower}
+                                   lbounds
+        in (Univ.LMap.remove r left, lbounds))
+      left (left, Univ.LMap.empty)
+  in
+  let rec instance (ctx, us, algs, insts, cstrs as acc) u =
+    let acc, left, lower =
+      match LMap.find u left with
+      | exception Not_found -> acc, [], LMap.empty
+      | l ->
+        let acc, left, newlow, lower =
+          List.fold_left
+          (fun (acc, left, newlow, lower') (d, l) ->
+           let acc', {enforce=enf;alg;lbound=l';lower} = aux acc l in
+           let l' =
+             if enf then Universe.make l
+             else l'
+           in acc', (d, l') :: left,
+              lower_add l d newlow, lower_union lower lower')
+          (acc, [], LMap.empty, LMap.empty) l
+        in
+        let left = CList.uniquize (List.filter (not_lower lower) left) in
+        (acc, left, LMap.union newlow lower)
+    in
+    let instantiate_lbound lbound =
+      let alg = LSet.mem u algs in
+        if alg then
+          (* u is algebraic: we instantiate it with its lower bound, if any,
+              or enforce the constraints if it is bounded from the top. *)
+          let lower = LSet.fold LMap.remove (Universe.levels lbound) lower in
+          instantiate_with_lbound u lbound lower ~alg:true ~enforce:false acc
+        else (* u is non algebraic *)
+          match Universe.level lbound with
+          | Some l -> (* The lowerbound is directly a level *)
+             (* u is not algebraic but has no upper bounds,
+                we instantiate it with its lower bound if it is a
+                different level, otherwise we keep it. *)
+             let lower = LMap.remove l lower in
+             if not (Level.equal l u) then
+               (* Should check that u does not
+                  have upper constraints that are not already in right *)
+               let acc = remove_alg l acc in
+                 instantiate_with_lbound u lbound lower ~alg:false ~enforce:false acc
+             else acc, {enforce=true; alg=false; lbound; lower}
+          | None ->
+            begin match find_inst insts lbound with
+              | can, lower ->
+                (* Another universe represents the same lower bound,
+                   we can share them with no harm. *)
+                let lower = LMap.remove can lower in
+                instantiate_with_lbound u (Universe.make can) lower ~alg:false ~enforce:false acc
+              | exception Not_found ->
+                (* We set u as the canonical universe representing lbound *)
+                instantiate_with_lbound u lbound lower ~alg:false ~enforce:true acc
+            end
+    in
+    let enforce_uppers ((ctx,us,algs,insts,cstrs), b as acc) =
+      match LMap.find u right with
+      | exception Not_found -> acc
+      | upper ->
+        let upper = List.filter (fun (d, r) -> not (LMap.mem r us)) upper in
+        let cstrs = enforce_uppers upper b.lbound cstrs in
+        (ctx, us, algs, insts, cstrs), b
+    in
+    if not (LSet.mem u ctx)
+    then enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
+    else
+      let lbound = compute_lbound left in
+      match lbound with
+      | None -> (* Nothing to do *)
+        enforce_uppers (acc, {enforce=true;alg=false;lbound=Universe.make u; lower})
+      | Some lbound ->
+        try enforce_uppers (instantiate_lbound lbound)
+        with UpperBoundedAlg ->
+          enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
+  and aux (ctx, us, algs, seen, cstrs as acc) u =
+    try acc, LMap.find u seen
+    with Not_found -> instance acc u
+  in
+    LMap.fold (fun u v (ctx, us, algs, seen, cstrs as acc) ->
+      if v == None then fst (aux acc u)
+      else LSet.remove u ctx, us, LSet.remove u algs, seen, cstrs)
+      us (ctx, us, algs, lbounds, cstrs)
+
+module UPairs = OrderedType.UnorderedPair(Univ.Level)
+module UPairSet = Set.Make (UPairs)
+
+let normalize_context_set g ctx us algs weak =
+  let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
+  (** Keep the Prop/Set <= i constraints separate for minimization *)
+  let smallles, csts =
+    Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts
+  in
+  let smallles = if is_set_minimization ()
+    then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx) smallles
+    else Constraint.empty
+  in
+  let csts, partition =
+    (* We first put constraints in a normal-form: all self-loops are collapsed
+       to equalities. *)
+    let g = LSet.fold (fun v g -> UGraph.add_universe v false g)
+                           ctx UGraph.initial_universes
+    in
+    let add_soft u g =
+      if not (Level.is_small u || LSet.mem u ctx)
+      then try UGraph.add_universe u false g with UGraph.AlreadyDeclared -> g
+      else g
+    in
+    let g = Constraint.fold
+        (fun (l, d, r) g -> add_soft r (add_soft l g))
+        csts g
+    in
+    let g = UGraph.merge_constraints csts g in
+      UGraph.constraints_of_universes g
+  in
+  (* We ignore the trivial Prop/Set <= i constraints. *)
+  let noneqs =
+    Constraint.filter
+      (fun (l,d,r) -> not ((d == Le && Level.is_small l) ||
+                           (Level.is_prop l && d == Lt && Level.is_set r)))
+      csts
+  in
+  let noneqs = Constraint.union noneqs smallles in
+  let flex x = LMap.mem x us in
+  let ctx, us, eqs = List.fold_left (fun (ctx, us, cstrs) s ->
+    let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in
+    (* Add equalities for globals which can't be merged anymore. *)
+    let cstrs = LSet.fold (fun g cst ->
+      Constraint.add (canon, Eq, g) cst) global
+      cstrs
+    in
+    (* Also add equalities for rigid variables *)
+    let cstrs = LSet.fold (fun g cst ->
+      Constraint.add (canon, Eq, g) cst) rigid
+      cstrs
+    in
+    let canonu = Some (Universe.make canon) in
+    let us = LSet.fold (fun f -> LMap.add f canonu) flexible us in
+      (LSet.diff ctx flexible, us, cstrs))
+    (ctx, us, Constraint.empty) partition
+  in
+  (* Process weak constraints: when one side is flexible and the 2
+     universes are unrelated unify them. *)
+  let ctx, us, g = UPairSet.fold (fun (u,v) (ctx, us, g as acc) ->
+      let norm = level_subst_of (normalize_univ_variable_opt_subst us) in
+      let u = norm u and v = norm v in
+      let set_to a b =
+        (LSet.remove a ctx,
+         LMap.add a (Some (Universe.make b)) us,
+         UGraph.enforce_constraint (a,Eq,b) g)
+      in
+      if UGraph.check_constraint g (u,Le,v) || UGraph.check_constraint g (v,Le,u)
+      then acc
+      else
+      if LMap.mem u us
+      then set_to u v
+      else if LMap.mem v us
+      then set_to v u
+      else acc)
+      weak (ctx, us, g)  in
+  (* Noneqs is now in canonical form w.r.t. equality constraints,
+     and contains only inequality constraints. *)
+  let noneqs =
+    let norm = level_subst_of (normalize_univ_variable_opt_subst us) in
+    Constraint.fold (fun (u,d,v) noneqs ->
+        let u = norm u and v = norm v in
+        if d != Lt && Level.equal u v then noneqs
+        else Constraint.add (u,d,v) noneqs)
+      noneqs Constraint.empty
+  in
+  (* Compute the left and right set of flexible variables, constraints
+     mentionning other variables remain in noneqs. *)
+  let noneqs, ucstrsl, ucstrsr =
+    Constraint.fold (fun (l,d,r as cstr) (noneq, ucstrsl, ucstrsr) ->
+      let lus = LMap.mem l us and rus = LMap.mem r us in
+      let ucstrsl' =
+        if lus then add_list_map l (d, r) ucstrsl
+        else ucstrsl
+      and ucstrsr' =
+        add_list_map r (d, l) ucstrsr
+      in
+      let noneqs =
+        if lus || rus then noneq
+        else Constraint.add cstr noneq
+      in (noneqs, ucstrsl', ucstrsr'))
+    noneqs (Constraint.empty, LMap.empty, LMap.empty)
+  in
+  (* Now we construct the instantiation of each variable. *)
+  let ctx', us, algs, inst, noneqs =
+    minimize_univ_variables ctx us algs ucstrsr ucstrsl noneqs
+  in
+  let us = normalize_opt_subst us in
+    (us, algs), (ctx', Constraint.union noneqs eqs)
+
+(* let normalize_conkey = CProfile.declare_profile "normalize_context_set" *)
+(* let normalize_context_set a b c = CProfile.profile3 normalize_conkey normalize_context_set a b c *)
diff --git a/engine/univMinim.mli b/engine/univMinim.mli
new file mode 100644
index 00000000..9f80b7ac
--- /dev/null
+++ b/engine/univMinim.mli
@@ -0,0 +1,32 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Univ
+open UnivSubst
+
+(** Unordered pairs of universe levels (ie (u,v) = (v,u)) *)
+module UPairSet : CSet.S with type elt = (Level.t * Level.t)
+
+(** Simplification and pruning of constraints:
+    [normalize_context_set ctx us]
+
+    - Instantiate the variables in [us] with their most precise
+    universe levels respecting the constraints.
+
+    - Normalizes the context [ctx] w.r.t. equality constraints,
+    choosing a canonical universe in each equivalence class
+    (a global one if there is one) and transitively saturate
+    the constraints w.r.t to the equalities. *)
+
+val normalize_context_set : UGraph.t -> ContextSet.t ->
+  universe_opt_subst (* The defined and undefined variables *) ->
+  LSet.t (* univ variables that can be substituted by algebraics *) ->
+  UPairSet.t (* weak equality constraints *) ->
+  (universe_opt_subst * LSet.t) in_universe_context_set
diff --git a/engine/univNames.ml b/engine/univNames.ml
new file mode 100644
index 00000000..a6884017
--- /dev/null
+++ b/engine/univNames.ml
@@ -0,0 +1,106 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+open Univ
+open Globnames
+open Nametab
+
+
+let qualid_of_level l =
+  match Level.name l with
+  | Some (d, n as na)  ->
+    begin
+    try Nametab.shortest_qualid_of_universe na
+    with Not_found ->
+      let name = Id.of_string_soft (string_of_int n) in
+      Libnames.make_qualid d name
+    end
+  | None ->
+    Libnames.qualid_of_ident @@ Id.of_string_soft (Level.to_string l)
+
+let pr_with_global_universes l = Libnames.pr_qualid (qualid_of_level l)
+
+(** Global universe information outside the kernel, to handle
+    polymorphic universe names in sections that have to be discharged. *)
+
+let universe_map = (Summary.ref UnivIdMap.empty ~name:"global universe info" : bool Nametab.UnivIdMap.t ref)
+
+let add_global_universe u p =
+  match Level.name u with
+  | Some n -> universe_map := Nametab.UnivIdMap.add n p !universe_map
+  | None -> ()
+
+let is_polymorphic l =
+  match Level.name l with
+  | Some n ->
+     (try Nametab.UnivIdMap.find n !universe_map
+      with Not_found -> false)
+  | None -> false
+
+(** Local universe names of polymorphic references *)
+
+type universe_binders = Univ.Level.t Names.Id.Map.t
+
+let empty_binders = Id.Map.empty
+
+let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders"
+
+let universe_binders_of_global ref : universe_binders =
+  try
+    let l = Refmap.find ref !universe_binders_table in l
+  with Not_found -> Names.Id.Map.empty
+
+let cache_ubinder (_,(ref,l)) =
+  universe_binders_table := Refmap.add ref l !universe_binders_table
+
+let subst_ubinder (subst,(ref,l as orig)) =
+  let ref' = fst (Globnames.subst_global subst ref) in
+  if ref == ref' then orig else ref', l
+
+let discharge_ubinder (_,(ref,l)) =
+  Some (Lib.discharge_global ref, l)
+
+let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj =
+  let open Libobject in
+  declare_object { (default_object "universe binder") with
+    cache_function = cache_ubinder;
+    load_function = (fun _ x -> cache_ubinder x);
+    classify_function = (fun x -> Substitute x);
+    subst_function = subst_ubinder;
+    discharge_function = discharge_ubinder;
+    rebuild_function = (fun x -> x); }
+
+let register_universe_binders ref ubinders =
+  (* Add the polymorphic (section) universes *)
+  let ubinders = UnivIdMap.fold (fun lvl poly ubinders ->
+    let qid = Nametab.shortest_qualid_of_universe lvl in
+    let level = Level.make (fst lvl) (snd lvl) in
+    if poly then Id.Map.add (snd (Libnames.repr_qualid qid)) level ubinders
+    else ubinders)
+    !universe_map ubinders
+  in
+  if not (Id.Map.is_empty ubinders)
+  then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders))
+
+type univ_name_list = Names.lname list
+
+let universe_binders_with_opt_names ref levels = function
+  | None -> universe_binders_of_global ref
+  | Some udecl ->
+    if Int.equal(List.length levels) (List.length udecl)
+    then
+      List.fold_left2 (fun acc { CAst.v = na} lvl -> match na with
+          | Anonymous -> acc
+          | Name na -> Names.Id.Map.add na lvl acc)
+        empty_binders udecl levels
+    else
+      CErrors.user_err ~hdr:"universe_binders_with_opt_names"
+        Pp.(str "Universe instance should have length " ++ int (List.length levels))
diff --git a/engine/univNames.mli b/engine/univNames.mli
new file mode 100644
index 00000000..837beac2
--- /dev/null
+++ b/engine/univNames.mli
@@ -0,0 +1,41 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Univ
+
+val pr_with_global_universes : Level.t -> Pp.t
+val qualid_of_level : Level.t -> Libnames.qualid
+
+(** Global universe information outside the kernel, to handle
+    polymorphic universes in sections that have to be discharged. *)
+val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit
+
+(** Is [lvl]  a global polymorphic universe? (ie section polymorphic universe) *)
+val is_polymorphic : Level.t -> bool
+
+(** Local universe name <-> level mapping *)
+
+type universe_binders = Univ.Level.t Names.Id.Map.t
+
+val empty_binders : universe_binders
+
+val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit
+val universe_binders_of_global : Names.GlobRef.t -> universe_binders
+
+type univ_name_list = Names.lname list
+
+(** [universe_binders_with_opt_names ref u l]
+
+    If [l] is [Some univs] return the universe binders naming the levels of [u] by [univs] (skipping Anonymous).
+    May error if the lengths mismatch.
+
+    Otherwise return [universe_binders_of_global ref]. *)
+val universe_binders_with_opt_names : Names.GlobRef.t ->
+  Univ.Level.t list -> univ_name_list option -> universe_binders
diff --git a/engine/univProblem.ml b/engine/univProblem.ml
new file mode 100644
index 00000000..bc2edc13
--- /dev/null
+++ b/engine/univProblem.ml
@@ -0,0 +1,166 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Univ
+open UnivSubst
+
+type t =
+  | ULe of Universe.t * Universe.t
+  | UEq of Universe.t * Universe.t
+  | ULub of Level.t * Level.t
+  | UWeak of Level.t * Level.t
+
+
+let is_trivial = function
+  | ULe (u, v) | UEq (u, v) -> Universe.equal u v
+  | ULub (u, v) | UWeak (u, v) -> Level.equal u v
+
+let subst_univs fn = function
+  | ULe (u, v) ->
+    let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
+    if Universe.equal u' v' then None
+    else Some (ULe (u',v'))
+  | UEq (u, v) ->
+    let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
+    if Universe.equal u' v' then None
+    else Some (ULe (u',v'))
+  | ULub (u, v) ->
+    let u' = level_subst_of fn u and v' = level_subst_of fn v in
+    if Level.equal u' v' then None
+    else Some (ULub (u',v'))
+  | UWeak (u, v) ->
+    let u' = level_subst_of fn u and v' = level_subst_of fn v in
+    if Level.equal u' v' then None
+    else Some (UWeak (u',v'))
+
+module Set = struct
+  module S = Set.Make(
+  struct
+    type nonrec t = t
+
+    let compare x y =
+      match x, y with
+      | ULe (u, v), ULe (u', v') ->
+        let i = Universe.compare u u' in
+        if Int.equal i 0 then Universe.compare v v'
+        else i
+      | UEq (u, v), UEq (u', v') ->
+        let i = Universe.compare u u' in
+        if Int.equal i 0 then Universe.compare v v'
+        else if Universe.equal u v' && Universe.equal v u' then 0
+        else i
+      | ULub (u, v), ULub (u', v') | UWeak (u, v), UWeak (u', v') ->
+        let i = Level.compare u u' in
+        if Int.equal i 0 then Level.compare v v'
+        else if Level.equal u v' && Level.equal v u' then 0
+        else i
+      | ULe _, _ -> -1
+      | _, ULe _ -> 1
+      | UEq _, _ -> -1
+      | _, UEq _ -> 1
+      | ULub _, _ -> -1
+      | _, ULub _ -> 1
+  end)
+
+  include S
+
+  let add cst s =
+    if is_trivial cst then s
+    else add cst s
+
+  let pr_one = let open Pp in function
+    | ULe (u, v) -> Universe.pr u ++ str " <= " ++ Universe.pr v
+    | UEq (u, v) -> Universe.pr u ++ str " = " ++ Universe.pr v
+    | ULub (u, v) -> Level.pr u ++ str " /\\ " ++ Level.pr v
+    | UWeak (u, v) -> Level.pr u ++ str " ~ " ++ Level.pr v
+
+  let pr c =
+    let open Pp in
+    fold (fun cst pp_std ->
+        pp_std ++ pr_one cst ++ fnl ()) c (str "")
+
+  let equal x y =
+    x == y || equal x y
+
+  let subst_univs subst csts =
+    fold
+      (fun c -> Option.fold_right add (subst_univs subst c))
+      csts empty
+end
+
+type 'a accumulator = Set.t -> 'a -> 'a option
+type 'a constrained = 'a * Set.t
+
+type 'a constraint_function = 'a -> 'a -> Set.t -> Set.t
+
+let enforce_eq_instances_univs strict x y c =
+  let mk u v = if strict then ULub (u, v) else UEq (Universe.make u, Universe.make v) in
+  let ax = Instance.to_array x and ay = Instance.to_array y in
+    if Array.length ax != Array.length ay then
+      CErrors.anomaly Pp.(str "Invalid argument: enforce_eq_instances_univs called with" ++
+                          str " instances of different lengths.");
+    CArray.fold_right2
+      (fun x y -> Set.add (mk x y))
+      ax ay c
+
+let to_constraints ~force_weak g s =
+  let invalid () =
+    raise (Invalid_argument "to_constraints: non-trivial algebraic constraint between universes")
+  in
+  let tr cst acc =
+    match cst with
+    | ULub (l, l') -> Constraint.add (l, Eq, l') acc
+    | UWeak (l, l') when force_weak -> Constraint.add (l, Eq, l') acc
+    | UWeak  _-> acc
+    | ULe (l, l') ->
+      begin match Universe.level l, Universe.level l' with
+        | Some l, Some l' -> Constraint.add (l, Le, l') acc
+        | None, Some _ -> enforce_leq l l' acc
+        | _, None ->
+          if UGraph.check_leq g l l'
+          then acc
+          else invalid ()
+      end
+    | UEq (l, l') ->
+      begin match Universe.level l, Universe.level l' with
+        | Some l, Some l' -> Constraint.add (l, Eq, l') acc
+        | None, _ | _, None ->
+          if UGraph.check_eq g l l'
+          then acc
+          else invalid ()
+      end
+  in
+  Set.fold tr s Constraint.empty
+
+
+(** Variant of [eq_constr_univs_infer] taking kind-of-term functions,
+    to expose subterms of [m] and [n], arguments. *)
+let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
+  (* spiwack: duplicates the code of [eq_constr_univs_infer] because I
+     haven't find a way to factor the code without destroying
+     pointer-equality optimisations in [eq_constr_univs_infer].
+     Pointer equality is not sufficient to ensure equality up to
+     [kind1,kind2], because [kind1] and [kind2] may be different,
+     typically evaluating [m] and [n] in different evar maps. *)
+  let cstrs = ref accu in
+  let eq_universes _ _ = 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
+      match fold (Set.singleton (UEq (u1, u2))) !cstrs with
+      | None -> false
+      | Some accu -> cstrs := accu; true
+  in
+  let rec eq_constr' nargs m n =
+    Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' nargs m n
+  in
+  let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' 0 m n in
+  if res then Some !cstrs else None
diff --git a/engine/univProblem.mli b/engine/univProblem.mli
new file mode 100644
index 00000000..ffaebe15
--- /dev/null
+++ b/engine/univProblem.mli
@@ -0,0 +1,55 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Constr
+open Univ
+
+(** {6 Constraints for type inference}
+
+    When doing conversion of universes, not only do we have =/<= constraints but
+    also Lub constraints which correspond to unification of two levels which might
+    not be necessary if unfolding is performed.
+
+    UWeak constraints come from irrelevant universes in cumulative polymorphism.
+*)
+
+type t =
+  | ULe of Universe.t * Universe.t
+  | UEq of Universe.t * Universe.t
+  | ULub of Level.t * Level.t
+  | UWeak of Level.t * Level.t
+
+val is_trivial : t -> bool
+
+module Set : sig
+  include Set.S with type elt = t
+
+  val pr : t -> Pp.t
+
+  val subst_univs : universe_subst_fn -> t -> t
+end
+
+type 'a accumulator = Set.t -> 'a -> 'a option
+type 'a constrained = 'a * Set.t
+type 'a constraint_function = 'a -> 'a -> Set.t -> Set.t
+
+val enforce_eq_instances_univs : bool -> Instance.t constraint_function
+
+(** With [force_weak] UWeak constraints are turned into equalities,
+   otherwise they're forgotten. *)
+val to_constraints : force_weak:bool -> UGraph.t -> Set.t -> Constraint.t
+
+(** [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
+    subterms of [m] and [n], arguments. *)
+val eq_constr_univs_infer_with :
+  (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
+  (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
+  UGraph.t -> 'a accumulator -> constr -> constr -> 'a -> 'a option
diff --git a/engine/univSubst.ml b/engine/univSubst.ml
new file mode 100644
index 00000000..2f59a3fa
--- /dev/null
+++ b/engine/univSubst.ml
@@ -0,0 +1,177 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Sorts
+open Util
+open Pp
+open Constr
+open Univ
+
+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
+
+let subst_univs_level fn l =
+  try Some (fn l)
+  with Not_found -> None
+
+let subst_univs_constraint fn (u,d,v as c) cstrs =
+  let u' = subst_univs_level fn u in
+  let v' = subst_univs_level fn v in
+  match u', v' with
+  | None, None -> Constraint.add c cstrs
+  | Some u, None -> enforce_univ_constraint (u,d,Universe.make v) cstrs
+  | None, Some v -> enforce_univ_constraint (Universe.make u,d,v) cstrs
+  | Some u, Some v -> enforce_univ_constraint (u,d,v) cstrs
+
+let subst_univs_constraints subst csts =
+  Constraint.fold
+    (fun c cstrs -> subst_univs_constraint subst c cstrs)
+    csts Constraint.empty
+
+let level_subst_of f =
+  fun l ->
+    try let u = f l in
+          match Universe.level u with
+          | None -> l
+          | Some l -> l
+    with Not_found -> l
+
+let subst_univs_fn_constr f c =
+  let changed = ref false in
+  let fu = Univ.subst_univs_universe f in
+  let fi = Univ.Instance.subst_fn (level_subst_of f) in
+  let rec aux t =
+    match kind t with
+    | Sort (Sorts.Type u) ->
+      let u' = fu u in
+        if u' == u then t else
+          (changed := true; mkSort (Sorts.sort_of_univ u'))
+    | Const (c, u) ->
+      let u' = fi u in
+        if u' == u then t
+        else (changed := true; mkConstU (c, u'))
+    | Ind (i, u) ->
+      let u' = fi u in
+        if u' == u then t
+        else (changed := true; mkIndU (i, u'))
+    | Construct (c, u) ->
+      let u' = fi u in
+        if u' == u then t
+        else (changed := true; mkConstructU (c, u'))
+    | _ -> map aux t
+  in
+  let c' = aux c in
+    if !changed then c' else c
+
+let subst_univs_constr subst c =
+  if Univ.is_empty_subst subst then c
+  else
+    let f = Univ.make_subst subst in
+      subst_univs_fn_constr f c
+
+let subst_univs_constr =
+  if Flags.profile then
+    let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in
+      CProfile.profile2 subst_univs_constr_key subst_univs_constr
+  else subst_univs_constr
+
+let normalize_univ_variable ~find =
+  let rec aux cur =
+    let b = find cur in
+    let b' = subst_univs_universe aux b in
+      if Universe.equal b' b then b
+      else b'
+  in aux
+
+let normalize_univ_variable_opt_subst ectx =
+  let find l =
+    match Univ.LMap.find l ectx with
+    | Some b -> b
+    | None -> raise Not_found
+  in
+  normalize_univ_variable ~find
+
+let normalize_univ_variable_subst subst =
+  let find l = Univ.LMap.find l subst in
+  normalize_univ_variable ~find
+
+let normalize_universe_opt_subst subst =
+  let normlevel = normalize_univ_variable_opt_subst subst in
+    subst_univs_universe normlevel
+
+let normalize_universe_subst subst =
+  let normlevel = normalize_univ_variable_subst subst in
+    subst_univs_universe normlevel
+
+let normalize_opt_subst ctx =
+  let normalize = normalize_universe_opt_subst ctx in
+  Univ.LMap.mapi (fun u -> function
+      | None -> None
+      | Some v -> Some (normalize v)) ctx
+
+type universe_opt_subst = Universe.t option universe_map
+
+let subst_univs_fn_puniverses f (c, u as cu) =
+  let u' = Instance.subst_fn f u in
+    if u' == u then cu else (c, u')
+
+let nf_evars_and_universes_opt_subst f subst =
+  let subst = normalize_univ_variable_opt_subst subst in
+  let lsubst = level_subst_of subst in
+  let rec aux c =
+    match kind c with
+    | Evar (evk, args) ->
+      let args = Array.map aux args in
+      (match try f (evk, args) with Not_found -> None with
+      | None -> mkEvar (evk, args)
+      | Some c -> aux c)
+    | Const pu ->
+      let pu' = subst_univs_fn_puniverses lsubst pu in
+        if pu' == pu then c else mkConstU pu'
+    | Ind pu ->
+      let pu' = subst_univs_fn_puniverses lsubst pu in
+        if pu' == pu then c else mkIndU pu'
+    | Construct pu ->
+      let pu' = subst_univs_fn_puniverses lsubst pu in
+        if pu' == pu then c else mkConstructU pu'
+    | Sort (Type u) ->
+      let u' = Univ.subst_univs_universe subst u in
+        if u' == u then c else mkSort (sort_of_univ u')
+    | _ -> Constr.map aux c
+  in aux
+
+let make_opt_subst s =
+  fun x ->
+    (match Univ.LMap.find x s with
+    | Some u -> u
+    | None -> raise Not_found)
+
+let subst_opt_univs_constr s =
+  let f = make_opt_subst s in
+  subst_univs_fn_constr f
+
+let normalize_univ_variables ctx =
+  let ctx = normalize_opt_subst ctx in
+  let def, subst =
+    Univ.LMap.fold (fun u v (def, subst) ->
+      match v with
+      | None -> (def, subst)
+      | Some b -> (Univ.LSet.add u def, Univ.LMap.add u b subst))
+    ctx (Univ.LSet.empty, Univ.LMap.empty)
+  in ctx, def, subst
+
+let pr_universe_body = function
+  | None -> mt ()
+  | Some v -> str" := " ++ Univ.Universe.pr v
+
+let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body
diff --git a/engine/univSubst.mli b/engine/univSubst.mli
new file mode 100644
index 00000000..e76d2533
--- /dev/null
+++ b/engine/univSubst.mli
@@ -0,0 +1,53 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Constr
+open Univ
+
+val level_subst_of : universe_subst_fn -> universe_level_subst_fn
+val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t
+
+val subst_univs_constr : universe_subst -> constr -> constr
+
+type universe_opt_subst = Universe.t option universe_map
+
+val make_opt_subst : universe_opt_subst -> universe_subst_fn
+
+val subst_opt_univs_constr : universe_opt_subst -> constr -> constr
+
+val normalize_univ_variables : universe_opt_subst ->
+  universe_opt_subst * LSet.t * universe_subst
+
+val normalize_univ_variable :
+  find:(Level.t -> Universe.t) ->
+  Level.t -> Universe.t
+
+val normalize_univ_variable_opt_subst : universe_opt_subst ->
+  (Level.t -> Universe.t)
+
+val normalize_univ_variable_subst : universe_subst ->
+  (Level.t -> Universe.t)
+
+val normalize_universe_opt_subst : universe_opt_subst ->
+  (Universe.t -> Universe.t)
+
+val normalize_universe_subst : universe_subst ->
+  (Universe.t -> Universe.t)
+
+val normalize_opt_subst : universe_opt_subst -> universe_opt_subst
+
+(** Full universes substitutions into terms *)
+
+val nf_evars_and_universes_opt_subst : (existential -> constr option) ->
+  universe_opt_subst -> constr -> constr
+
+(** Pretty-printing *)
+
+val pr_universe_opt_subst : universe_opt_subst -> Pp.t
diff --git a/engine/universes.ml b/engine/universes.ml
index fb64a642..ee966843 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -8,1129 +8,90 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Sorts
-open Util
-open Pp
-open Names
-open Constr
-open Environ
 open Univ
-open Globnames
-open Nametab
 
-module UPairs = OrderedType.UnorderedPair(Univ.Level)
-module UPairSet = Set.Make (UPairs)
-
-let reference_of_level l = CAst.make @@
-  match Level.name l with
-  | Some (d, n as na)  ->
-     let qid =
-       try Nametab.shortest_qualid_of_universe na
-       with Not_found ->
-         let name = Id.of_string_soft (string_of_int n) in
-         Libnames.make_qualid d name
-     in Libnames.Qualid qid
-  | None -> Libnames.Ident Id.(of_string_soft (Level.to_string l))
-
-let pr_with_global_universes l = Libnames.pr_reference (reference_of_level l)
-
-(** Global universe information outside the kernel, to handle
-    polymorphic universe names in sections that have to be discharged. *)
-
-let universe_map = (Summary.ref UnivIdMap.empty ~name:"global universe info" : bool Nametab.UnivIdMap.t ref)
-
-let add_global_universe u p =
-  match Level.name u with
-  | Some n -> universe_map := Nametab.UnivIdMap.add n p !universe_map
-  | None -> ()
-
-let is_polymorphic l =
-  match Level.name l with
-  | Some n ->
-     (try Nametab.UnivIdMap.find n !universe_map
-      with Not_found -> false)
-  | None -> false
-
-(** Local universe names of polymorphic references *)
-
-type universe_binders = Univ.Level.t Names.Id.Map.t
-
-let empty_binders = Id.Map.empty
-
-let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders"
-
-let universe_binders_of_global ref : universe_binders =
-  try
-    let l = Refmap.find ref !universe_binders_table in l
-  with Not_found -> Names.Id.Map.empty
-
-let cache_ubinder (_,(ref,l)) =
-  universe_binders_table := Refmap.add ref l !universe_binders_table
-
-let subst_ubinder (subst,(ref,l as orig)) =
-  let ref' = fst (Globnames.subst_global subst ref) in
-  if ref == ref' then orig else ref', l
-
-let discharge_ubinder (_,(ref,l)) =
-  Some (Lib.discharge_global ref, l)
-
-let ubinder_obj : Globnames.global_reference * universe_binders -> Libobject.obj =
-  let open Libobject in
-  declare_object { (default_object "universe binder") with
-    cache_function = cache_ubinder;
-    load_function = (fun _ x -> cache_ubinder x);
-    classify_function = (fun x -> Substitute x);
-    subst_function = subst_ubinder;
-    discharge_function = discharge_ubinder;
-    rebuild_function = (fun x -> x); }
-
-let register_universe_binders ref ubinders =
-  let open Names in
-  (* Add the polymorphic (section) universes *)
-  let ubinders = UnivIdMap.fold (fun lvl poly ubinders ->
-    let qid = Nametab.shortest_qualid_of_universe lvl in
-    let level = Level.make (fst lvl) (snd lvl) in
-    if poly then Id.Map.add (snd (Libnames.repr_qualid qid)) level ubinders
-    else ubinders)
-    !universe_map ubinders
-  in
-  if not (Id.Map.is_empty ubinders)
-  then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders))
-
-type univ_name_list = Misctypes.lname list
-
-let universe_binders_with_opt_names ref levels = function
-  | None -> universe_binders_of_global ref
-  | Some udecl ->
-    if Int.equal(List.length levels) (List.length udecl)
-    then
-      List.fold_left2 (fun acc { CAst.v = na} lvl -> match na with
-          | Anonymous -> acc
-          | Name na -> Names.Id.Map.add na lvl acc)
-        empty_binders udecl levels
-    else
-      CErrors.user_err ~hdr:"universe_binders_with_opt_names"
-        Pp.(str "Universe instance should have length " ++ int (List.length levels))
-
-(* To disallow minimization to Set *)
-
-let set_minimization = ref true
-let is_set_minimization () = !set_minimization
-			    
-type universe_constraint =
+(** Deprecated *)
+
+(** UnivNames *)
+type universe_binders = UnivNames.universe_binders
+type univ_name_list = UnivNames.univ_name_list
+
+let pr_with_global_universes = UnivNames.pr_with_global_universes
+let reference_of_level = UnivNames.qualid_of_level
+
+let add_global_universe = UnivNames.add_global_universe
+
+let is_polymorphic = UnivNames.is_polymorphic
+
+let empty_binders = UnivNames.empty_binders
+
+let register_universe_binders = UnivNames.register_universe_binders
+let universe_binders_of_global = UnivNames.universe_binders_of_global
+
+let universe_binders_with_opt_names = UnivNames.universe_binders_with_opt_names
+
+(** UnivGen *)
+type universe_id = UnivGen.universe_id
+
+let set_remote_new_univ_id = UnivGen.set_remote_new_univ_id
+let new_univ_id = UnivGen.new_univ_id
+let new_univ_level = UnivGen.new_univ_level
+let new_univ = UnivGen.new_univ
+let new_Type = UnivGen.new_Type
+let new_Type_sort = UnivGen.new_Type_sort
+let new_global_univ = UnivGen.new_global_univ
+let new_sort_in_family = UnivGen.new_sort_in_family
+let fresh_instance_from_context = UnivGen.fresh_instance_from_context
+let fresh_instance_from = UnivGen.fresh_instance_from
+let fresh_sort_in_family = UnivGen.fresh_sort_in_family
+let fresh_constant_instance = UnivGen.fresh_constant_instance
+let fresh_inductive_instance = UnivGen.fresh_inductive_instance
+let fresh_constructor_instance = UnivGen.fresh_constructor_instance
+let fresh_global_instance = UnivGen.fresh_global_instance
+let fresh_global_or_constr_instance = UnivGen.fresh_global_or_constr_instance
+let fresh_universe_context_set_instance = UnivGen.fresh_universe_context_set_instance
+let global_of_constr = UnivGen.global_of_constr
+let constr_of_global_univ = UnivGen.constr_of_global_univ
+let extend_context = UnivGen.extend_context
+let constr_of_global = UnivGen.constr_of_global
+let constr_of_reference = UnivGen.constr_of_global
+let type_of_global = UnivGen.type_of_global
+
+(** UnivSubst *)
+
+let level_subst_of = UnivSubst.level_subst_of
+let subst_univs_constraints = UnivSubst.subst_univs_constraints
+let subst_univs_constr = UnivSubst.subst_univs_constr
+type universe_opt_subst = UnivSubst.universe_opt_subst
+let make_opt_subst = UnivSubst.make_opt_subst
+let subst_opt_univs_constr = UnivSubst.subst_opt_univs_constr
+let normalize_univ_variables = UnivSubst.normalize_univ_variables
+let normalize_univ_variable = UnivSubst.normalize_univ_variable
+let normalize_univ_variable_opt_subst = UnivSubst.normalize_univ_variable_opt_subst
+let normalize_univ_variable_subst = UnivSubst.normalize_univ_variable_subst
+let normalize_universe_opt_subst = UnivSubst.normalize_universe_opt_subst
+let normalize_universe_subst = UnivSubst.normalize_universe_subst
+let nf_evars_and_universes_opt_subst = UnivSubst.nf_evars_and_universes_opt_subst
+let pr_universe_opt_subst = UnivSubst.pr_universe_opt_subst
+
+(** UnivProblem *)
+
+type universe_constraint = UnivProblem.t =
   | ULe of Universe.t * Universe.t
   | UEq of Universe.t * Universe.t
   | ULub of Level.t * Level.t
   | UWeak of Level.t * Level.t
 
-module Constraints = struct
-  module S = Set.Make(
-  struct 
-    type t = universe_constraint
-
-    let compare x y =
-      match x, y with
-      | ULe (u, v), ULe (u', v') ->
-        let i = Universe.compare u u' in
-        if Int.equal i 0 then Universe.compare v v'
-        else i
-      | UEq (u, v), UEq (u', v') ->
-        let i = Universe.compare u u' in
-        if Int.equal i 0 then Universe.compare v v'
-        else if Universe.equal u v' && Universe.equal v u' then 0
-        else i
-      | ULub (u, v), ULub (u', v') | UWeak (u, v), UWeak (u', v') ->
-        let i = Level.compare u u' in
-        if Int.equal i 0 then Level.compare v v'
-        else if Level.equal u v' && Level.equal v u' then 0
-        else i
-      | ULe _, _ -> -1
-      | _, ULe _ -> 1
-      | UEq _, _ -> -1
-      | _, UEq _ -> 1
-      | ULub _, _ -> -1
-      | _, ULub _ -> 1
-  end)
-  
-  include S
-
-  let is_trivial = function
-    | ULe (u, v) | UEq (u, v) -> Universe.equal u v
-    | ULub (u, v) | UWeak (u, v) -> Level.equal u v
-
-  let add cst s =
-    if is_trivial cst then s
-    else add cst s
-
-  let pr_one = function
-    | ULe (u, v) -> Universe.pr u ++ str " <= " ++ Universe.pr v
-    | UEq (u, v) -> Universe.pr u ++ str " = " ++ Universe.pr v
-    | ULub (u, v) -> Level.pr u ++ str " /\\ " ++ Level.pr v
-    | UWeak (u, v) -> Level.pr u ++ str " ~ " ++ Level.pr v
-
-  let pr c =
-    fold (fun cst pp_std ->
-        pp_std ++ pr_one cst ++ fnl ()) c (str "")
-
-  let equal x y = 
-    x == y || equal x y
-
-end
-
-type universe_constraints = Constraints.t
-type 'a constraint_accumulator = universe_constraints -> 'a -> 'a option
-type 'a universe_constrained = 'a * universe_constraints
-
-type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints
-
-let enforce_eq_instances_univs strict x y c = 
-  let mk u v = if strict then ULub (u, v) else UEq (Universe.make u, Universe.make v) in
-  let ax = Instance.to_array x and ay = Instance.to_array y in
-    if Array.length ax != Array.length ay then
-      CErrors.anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with" ++
-	       Pp.str " instances of different lengths.");
-    CArray.fold_right2
-      (fun x y -> Constraints.add (mk x y))
-      ax ay 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
-
-let subst_univs_level fn l =
-  try Some (fn l)
-  with Not_found -> None
-
-let subst_univs_constraint fn (u,d,v as c) cstrs =
-  let u' = subst_univs_level fn u in
-  let v' = subst_univs_level fn v in
-  match u', v' with
-  | None, None -> Constraint.add c cstrs
-  | Some u, None -> enforce_univ_constraint (u,d,Universe.make v) cstrs
-  | None, Some v -> enforce_univ_constraint (Universe.make u,d,v) cstrs
-  | Some u, Some v -> enforce_univ_constraint (u,d,v) cstrs
-
-let subst_univs_constraints subst csts =
-  Constraint.fold
-    (fun c cstrs -> subst_univs_constraint subst c cstrs)
-    csts Constraint.empty
-
-let level_subst_of f =
-  fun l ->
-    try let u = f l in
-          match Universe.level u with
-          | None -> l
-          | Some l -> l
-    with Not_found -> l
-
-let subst_univs_universe_constraint fn = function
-  | ULe (u, v) ->
-    let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
-    if Universe.equal u' v' then None
-    else Some (ULe (u',v'))
-  | UEq (u, v) ->
-    let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
-    if Universe.equal u' v' then None
-    else Some (ULe (u',v'))
-  | ULub (u, v) ->
-    let u' = level_subst_of fn u and v' = level_subst_of fn v in
-    if Level.equal u' v' then None
-    else Some (ULub (u',v'))
-  | UWeak (u, v) ->
-    let u' = level_subst_of fn u and v' = level_subst_of fn v in
-    if Level.equal u' v' then None
-    else Some (UWeak (u',v'))
-
-let subst_univs_universe_constraints subst csts =
-  Constraints.fold 
-    (fun c -> Option.fold_right Constraints.add (subst_univs_universe_constraint subst c))
-    csts Constraints.empty 
-
-let to_constraints ~force_weak g s =
-  let invalid () =
-    raise (Invalid_argument "to_constraints: non-trivial algebraic constraint between universes")
-  in
-  let tr cst acc =
-    match cst with
-    | ULub (l, l') -> Constraint.add (l, Eq, l') acc
-    | UWeak (l, l') when force_weak -> Constraint.add (l, Eq, l') acc
-    | UWeak  _-> acc
-    | ULe (l, l') ->
-      begin match Universe.level l, Universe.level l' with
-        | Some l, Some l' -> Constraint.add (l, Le, l') acc
-        | None, Some _ -> enforce_leq l l' acc
-        | _, None ->
-          if UGraph.check_leq g l l'
-          then acc
-          else invalid ()
-      end
-    | UEq (l, l') ->
-      begin match Universe.level l, Universe.level l' with
-        | Some l, Some l' -> Constraint.add (l, Eq, l') acc
-        | None, _ | _, None ->
-          if UGraph.check_eq g l l'
-          then acc
-          else invalid ()
-      end
-  in
-  Constraints.fold tr s Constraint.empty
-
-(** Variant of [eq_constr_univs_infer] taking kind-of-term functions,
-    to expose subterms of [m] and [n], arguments. *)
-let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
-  (* spiwack: duplicates the code of [eq_constr_univs_infer] because I
-     haven't find a way to factor the code without destroying
-     pointer-equality optimisations in [eq_constr_univs_infer].
-     Pointer equality is not sufficient to ensure equality up to
-     [kind1,kind2], because [kind1] and [kind2] may be different,
-     typically evaluating [m] and [n] in different evar maps. *)
-  let cstrs = ref accu in
-  let eq_universes _ _ = 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
-      match fold (Constraints.singleton (UEq (u1, u2))) !cstrs with
-      | None -> false
-      | Some accu -> cstrs := accu; true
-  in
-  let rec eq_constr' nargs m n =
-    Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' nargs m n
-  in
-  let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' 0 m n in
-  if res then Some !cstrs else None
-
-(* Generator of levels *)
-type universe_id = DirPath.t * int
-
-let new_univ_id, set_remote_new_univ_id =
-  RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1)
-    ~build:(fun n -> Global.current_dirpath (), n)
-
-let new_univ_level () =
-  let dp, id = new_univ_id () in
-  Univ.Level.make dp id
-
-let fresh_level () = new_univ_level ()
-
-(* TODO: remove *)
-let new_univ dp = Univ.Universe.make (new_univ_level dp)
-let new_Type dp = mkType (new_univ dp)
-let new_Type_sort dp = Type (new_univ dp)
-
-let fresh_universe_instance ctx =
-  let init _ = new_univ_level () in
-  Instance.of_array (Array.init (AUContext.size ctx) init)
-
-let fresh_instance_from_context ctx =
-  let inst = fresh_universe_instance ctx in
-  let constraints = AUContext.instantiate inst ctx in
-    inst, constraints
-
-let fresh_instance ctx =
-  let ctx' = ref LSet.empty in
-  let init _ =
-    let u = new_univ_level () in
-    ctx' := LSet.add u !ctx'; u
-  in
-  let inst = Instance.of_array (Array.init (AUContext.size ctx) init)
-  in !ctx', inst
-
-let existing_instance ctx inst = 
-  let () = 
-    let len1 = Array.length (Instance.to_array inst)
-    and len2 = AUContext.size ctx in
-      if not (len1 == len2) then
-	CErrors.user_err ~hdr:"Universes"
-	  (str "Polymorphic constant expected " ++ int len2 ++ 
-	     str" levels but was given " ++ int len1)
-      else ()
-  in LSet.empty, inst
-
-let fresh_instance_from ctx inst =
-  let ctx', inst = 
-    match inst with 
-    | Some inst -> existing_instance ctx inst
-    | None -> fresh_instance ctx 
-  in
-  let constraints = AUContext.instantiate inst ctx in
-    inst, (ctx', constraints)
-
-(** Fresh universe polymorphic construction *)
-
-let fresh_constant_instance env c inst =
-  let cb = lookup_constant c env in
-  match cb.Declarations.const_universes with
-  | Declarations.Monomorphic_const _ -> ((c,Instance.empty), ContextSet.empty)
-  | Declarations.Polymorphic_const auctx -> 
-    let inst, ctx =
-      fresh_instance_from auctx inst
-    in
-    ((c, inst), ctx)
-
-let fresh_inductive_instance env ind inst = 
-  let mib, mip = Inductive.lookup_mind_specif env ind in
-  match mib.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ ->
-    ((ind,Instance.empty), ContextSet.empty)
-  | Declarations.Polymorphic_ind uactx ->
-    let inst, ctx = (fresh_instance_from uactx) inst in 
-     ((ind,inst), ctx)
-  | Declarations.Cumulative_ind acumi ->
-    let inst, ctx = 
-      fresh_instance_from (Univ.ACumulativityInfo.univ_context acumi) inst
-    in ((ind,inst), ctx)
-
-let fresh_constructor_instance env (ind,i) inst = 
-  let mib, mip = Inductive.lookup_mind_specif env ind in
-  match mib.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ -> (((ind,i),Instance.empty), ContextSet.empty)
-  | Declarations.Polymorphic_ind auctx ->
-    let inst, ctx = fresh_instance_from auctx  inst in
-	(((ind,i),inst), ctx)
-  | Declarations.Cumulative_ind acumi ->
-    let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in
-    (((ind,i),inst), ctx)
-
-open Globnames
-
-let fresh_global_instance ?names env gr =
-  match gr with
-  | VarRef id -> mkVar id, ContextSet.empty
-  | ConstRef sp -> 
-     let c, ctx = fresh_constant_instance env sp names in
-       mkConstU c, ctx
-  | ConstructRef sp ->
-     let c, ctx = fresh_constructor_instance env sp names in
-       mkConstructU c, ctx
-  | IndRef sp -> 
-     let c, ctx = fresh_inductive_instance env sp names in
-       mkIndU c, ctx
-
-let fresh_constant_instance env sp = 
-  fresh_constant_instance env sp None
-
-let fresh_inductive_instance env sp = 
-  fresh_inductive_instance env sp None
-
-let fresh_constructor_instance env sp = 
-  fresh_constructor_instance env sp None
-
-let constr_of_global gr =
-  let c, ctx = fresh_global_instance (Global.env ()) gr in
-    if not (Univ.ContextSet.is_empty ctx) then
-      if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then 
-	(* Should be an error as we might forget constraints, allow for now
-	   to make firstorder work with "using" clauses *)
-	c
-      else CErrors.user_err ~hdr:"constr_of_global"
-          Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
-	      str " would forget universes.")
-    else c
-
-let constr_of_reference = constr_of_global
-
-let constr_of_global_univ (gr,u) =
-  match gr with
-  | VarRef id -> mkVar id
-  | ConstRef sp -> mkConstU (sp,u)
-  | ConstructRef sp -> mkConstructU (sp,u)
-  | IndRef sp -> mkIndU (sp,u)
-
-let fresh_global_or_constr_instance env = function
-  | IsConstr c -> c, ContextSet.empty
-  | IsGlobal gr -> fresh_global_instance env gr
-
-let global_of_constr c =
-  match kind c with
-  | Const (c, u) -> ConstRef c, u
-  | Ind (i, u) -> IndRef i, u
-  | Construct (c, u) -> ConstructRef c, u
-  | Var id -> VarRef id, Instance.empty
-  | _ -> raise Not_found
-
-open Declarations
-
-let type_of_reference env r =
-  match r with
-  | VarRef id -> Environ.named_type id env, ContextSet.empty
-  | ConstRef c ->
-     let cb = Environ.lookup_constant c env in
-     let ty = cb.const_type in
-     begin
-       match cb.const_universes with
-       | Monomorphic_const _ -> ty, ContextSet.empty
-       | Polymorphic_const auctx ->
-         let inst, ctx = fresh_instance_from auctx None in
-         Vars.subst_instance_constr inst ty, ctx
-     end
-  | IndRef ind ->
-     let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
-     begin
-       match mib.mind_universes with
-       | Monomorphic_ind _ ->
-         let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in
-	 ty, ContextSet.empty
-       | Polymorphic_ind auctx ->
-         let inst, ctx = fresh_instance_from auctx  None in
-	 let ty = Inductive.type_of_inductive env (specif, inst) in
-         ty, ctx
-       | Cumulative_ind cumi ->
-         let inst, ctx = 
-           fresh_instance_from (ACumulativityInfo.univ_context cumi) None
-         in
-         let ty = Inductive.type_of_inductive env (specif, inst) in
-         ty, ctx
-     end
-	 
-  | ConstructRef cstr ->
-    let (mib,oib as specif) = 
-      Inductive.lookup_mind_specif env (inductive_of_constructor cstr) 
-    in
-    begin
-       match mib.mind_universes with
-       | Monomorphic_ind _ ->
-         Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty
-       | Polymorphic_ind auctx ->
-         let inst, ctx = fresh_instance_from auctx None in
-	 Inductive.type_of_constructor (cstr,inst) specif, ctx
-       | Cumulative_ind cumi ->
-         let inst, ctx = 
-           fresh_instance_from (ACumulativityInfo.univ_context cumi) None 
-         in
-	 Inductive.type_of_constructor (cstr,inst) specif, ctx
-     end
-
-let type_of_global t = type_of_reference (Global.env ()) t
-
-let fresh_sort_in_family env = function
-  | InProp -> Sorts.prop, ContextSet.empty
-  | InSet -> Sorts.set, ContextSet.empty
-  | InType -> 
-    let u = fresh_level () in
-      Type (Univ.Universe.make u), ContextSet.singleton u
-
-let new_sort_in_family sf =
-  fst (fresh_sort_in_family (Global.env ()) sf)
-
-let extend_context (a, ctx) (ctx') =
-  (a, ContextSet.union ctx ctx')
-
-let new_global_univ () =
-  let u = fresh_level () in
-    (Univ.Universe.make u, ContextSet.singleton u)
-
-(** Simplification *)
-
-module LevelUnionFind = Unionfind.Make (Univ.LSet) (Univ.LMap)
-
-let add_list_map u t map =
-  try
-    let l = LMap.find u map in
-    LMap.set u (t :: l) map
-  with Not_found ->
-    LMap.add u [t] map
-
-module UF = LevelUnionFind
-
-(** Precondition: flexible <= ctx *)
-let choose_canonical ctx flexible algs s =
-  let global = LSet.diff s ctx in
-  let flexible, rigid = LSet.partition flexible (LSet.inter s ctx) in
-    (** If there is a global universe in the set, choose it *)
-    if not (LSet.is_empty global) then
-      let canon = LSet.choose global in
-	canon, (LSet.remove canon global, rigid, flexible)
-    else (** No global in the equivalence class, choose a rigid one *)
-	if not (LSet.is_empty rigid) then
-	  let canon = LSet.choose rigid in
-	    canon, (global, LSet.remove canon rigid, flexible)
-	else (** There are only flexible universes in the equivalence
-		 class, choose a non-algebraic. *)
-	  let algs, nonalgs = LSet.partition (fun x -> LSet.mem x algs) flexible in
-	    if not (LSet.is_empty nonalgs) then
-	      let canon = LSet.choose nonalgs in
-		canon, (global, rigid, LSet.remove canon flexible)
-	    else
-	      let canon = LSet.choose algs in
-		canon, (global, rigid, LSet.remove canon flexible)
-
-let subst_univs_fn_constr f c =
-  let changed = ref false in
-  let fu = Univ.subst_univs_universe f in
-  let fi = Univ.Instance.subst_fn (level_subst_of f) in
-  let rec aux t =
-    match kind t with
-    | Sort (Sorts.Type u) ->
-      let u' = fu u in
-        if u' == u then t else
-          (changed := true; mkSort (Sorts.sort_of_univ u'))
-    | Const (c, u) ->
-      let u' = fi u in
-        if u' == u then t
-        else (changed := true; mkConstU (c, u'))
-    | Ind (i, u) ->
-      let u' = fi u in
-        if u' == u then t
-        else (changed := true; mkIndU (i, u'))
-    | Construct (c, u) ->
-      let u' = fi u in
-        if u' == u then t
-        else (changed := true; mkConstructU (c, u'))
-    | _ -> map aux t
-  in
-  let c' = aux c in
-    if !changed then c' else c
-
-let subst_univs_constr subst c =
-  if Univ.is_empty_subst subst then c
-  else
-    let f = Univ.make_subst subst in
-      subst_univs_fn_constr f c
-
-let subst_univs_constr =
-  if Flags.profile then
-    let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in
-      CProfile.profile2 subst_univs_constr_key subst_univs_constr
-  else subst_univs_constr
-
-let fresh_universe_context_set_instance ctx =
-  if ContextSet.is_empty ctx then LMap.empty, ctx
-  else
-    let (univs, cst) = ContextSet.levels ctx, ContextSet.constraints ctx in
-    let univs',subst = LSet.fold
-      (fun u (univs',subst) ->
-	let u' = fresh_level () in
-	  (LSet.add u' univs', LMap.add u u' subst))
-      univs (LSet.empty, LMap.empty)
-    in
-    let cst' = subst_univs_level_constraints subst cst in
-      subst, (univs', cst')
-
-let normalize_univ_variable ~find ~update =
-  let rec aux cur =
-    let b = find cur in
-    let b' = subst_univs_universe aux b in
-      if Universe.equal b' b then b
-      else update cur b'
-  in aux
-
-let normalize_univ_variable_opt_subst ectx =
-  let find l = 
-    match Univ.LMap.find l !ectx with
-    | Some b -> b
-    | None -> raise Not_found
-  in
-  let update l b =
-    assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true);
-    try ectx := Univ.LMap.add l (Some b) !ectx; b with Not_found -> assert false
-  in normalize_univ_variable ~find ~update
-
-let normalize_univ_variable_subst subst =
-  let find l = Univ.LMap.find l !subst in
-  let update l b =
-    assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true);
-    try subst := Univ.LMap.set l b !subst; b with Not_found -> assert false in
-    normalize_univ_variable ~find ~update
-
-let normalize_universe_opt_subst subst =
-  let normlevel = normalize_univ_variable_opt_subst subst in
-    subst_univs_universe normlevel
-
-let normalize_universe_subst subst =
-  let normlevel = normalize_univ_variable_subst subst in
-    subst_univs_universe normlevel
-
-let normalize_opt_subst ctx = 
-  let ectx = ref ctx in
-  let normalize = normalize_univ_variable_opt_subst ectx in
-  let () =
-    Univ.LMap.iter (fun u v ->
-      if Option.is_empty v then ()
-      else try ignore(normalize u) with Not_found -> assert(false)) ctx 
-  in !ectx
-
-type universe_opt_subst = Universe.t option universe_map
-
-let subst_univs_fn_puniverses f (c, u as cu) =
-  let u' = Instance.subst_fn f u in
-    if u' == u then cu else (c, u')
-
-let nf_evars_and_universes_opt_subst f subst =
-  let subst = normalize_univ_variable_opt_subst (ref subst) in
-  let lsubst = level_subst_of subst in
-  let rec aux c =
-    match kind c with
-    | Evar (evk, args) ->
-      let args = Array.map aux args in
-      (match try f (evk, args) with Not_found -> None with
-      | None -> mkEvar (evk, args)
-      | Some c -> aux c)
-    | Const pu ->
-      let pu' = subst_univs_fn_puniverses lsubst pu in
-        if pu' == pu then c else mkConstU pu'
-    | Ind pu ->
-      let pu' = subst_univs_fn_puniverses lsubst pu in
-        if pu' == pu then c else mkIndU pu'
-    | Construct pu ->
-      let pu' = subst_univs_fn_puniverses lsubst pu in
-        if pu' == pu then c else mkConstructU pu'
-    | Sort (Type u) ->
-      let u' = Univ.subst_univs_universe subst u in
-        if u' == u then c else mkSort (sort_of_univ u')
-    | _ -> Constr.map aux c
-  in aux
-
-let make_opt_subst s = 
-  fun x -> 
-    (match Univ.LMap.find x s with
-    | Some u -> u
-    | None -> raise Not_found)
-
-let subst_opt_univs_constr s = 
-  let f = make_opt_subst s in
-  subst_univs_fn_constr f
-
-let normalize_univ_variables ctx = 
-  let ctx = normalize_opt_subst ctx in
-  let undef, def, subst =
-    Univ.LMap.fold (fun u v (undef, def, subst) -> 
-      match v with
-      | None -> (Univ.LSet.add u undef, def, subst)
-      | Some b -> (undef, Univ.LSet.add u def, Univ.LMap.add u b subst))
-    ctx (Univ.LSet.empty, Univ.LSet.empty, Univ.LMap.empty)
-  in ctx, undef, def, subst
-
-let pr_universe_body = function
-  | None -> mt ()
-  | Some v -> str" := " ++ Univ.Universe.pr v
-
-let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body
-
-let compare_constraint_type d d' =
-  match d, d' with
-  | Eq, Eq -> 0
-  | Eq, _ -> -1
-  | _, Eq -> 1
-  | Le, Le -> 0
-  | Le, _ -> -1
-  | _, Le -> 1
-  | Lt, Lt -> 0
-
-type lowermap = constraint_type LMap.t
-
-let lower_union =
-  let merge k a b =
-    match a, b with
-    | Some _, None -> a
-    | None, Some _ -> b
-    | None, None -> None
-    | Some l, Some r ->
-       if compare_constraint_type l r >= 0 then a
-       else b
-  in LMap.merge merge
-
-let lower_add l c m =
-  try let c' = LMap.find l m in
-      if compare_constraint_type c c' > 0 then
-        LMap.add l c m
-      else m
-  with Not_found -> LMap.add l c m
-
-let lower_of_list l =
-  List.fold_left (fun acc (d,l) -> LMap.add l d acc) LMap.empty l
-
-exception Found of Level.t * lowermap
-let find_inst insts v =
-  try LMap.iter (fun k (enf,alg,v',lower) ->
-    if not alg && enf && Universe.equal v' v then raise (Found (k, lower)))
-	insts; raise Not_found
-  with Found (f,l) -> (f,l)
-
-let compute_lbound left =
- (** The universe variable was not fixed yet.
-     Compute its level using its lower bound. *)
-  let sup l lbound = 
-    match lbound with
-    | None -> Some l
-    | Some l' -> Some (Universe.sup l l')
-  in
-    List.fold_left (fun lbound (d, l) -> 
-      if d == Le (* l <= ?u *) then sup l lbound
-      else (* l < ?u *) 
-	(assert (d == Lt); 
-	 if not (Universe.level l == None) then
-	   sup (Universe.super l) lbound
-	 else None))
-      None left
-  
-let instantiate_with_lbound u lbound lower alg enforce (ctx, us, algs, insts, cstrs) =
-  if enforce then
-    let inst = Universe.make u in
-    let cstrs' = enforce_leq lbound inst cstrs in
-      (ctx, us, LSet.remove u algs, 
-       LMap.add u (enforce,alg,lbound,lower) insts, cstrs'),
-      (enforce, alg, inst, lower)
-  else (* Actually instantiate *)
-    (Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs,
-     LMap.add u (enforce,alg,lbound,lower) insts, cstrs),
-    (enforce, alg, lbound, lower)
-
-type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t
-
-let _pr_constraints_map (cmap:constraints_map) =
-  LMap.fold (fun l cstrs acc -> 
-    Level.pr l ++ str " => " ++ 
-      prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++
-      fnl () ++ acc)
-    cmap (mt ())
-
-let remove_alg l (ctx, us, algs, insts, cstrs) =
-  (ctx, us, LSet.remove l algs, insts, cstrs)
-
-let remove_lower u lower =
-  let levels = Universe.levels u in
-  LSet.fold (fun l acc -> LMap.remove l acc) levels lower
-    
-let minimize_univ_variables ctx us algs left right cstrs =
-  let left, lbounds = 
-    Univ.LMap.fold (fun r lower (left, lbounds as acc)  ->
-      if Univ.LMap.mem r us || not (Univ.LSet.mem r ctx) then acc
-      else (* Fixed universe, just compute its glb for sharing *)
-	let lbounds' = 
-	  match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with
-	  | None -> lbounds
-	  | Some lbound -> LMap.add r (true, false, lbound, lower_of_list lower)
-                                   lbounds
-	in (Univ.LMap.remove r left, lbounds'))
-      left (left, Univ.LMap.empty)
-  in
-  let rec instance (ctx', us, algs, insts, cstrs as acc) u =
-    let acc, left, lower =
-      try
-        let l = LMap.find u left in
-	let acc, left, newlow, lower =
-          List.fold_left
-	  (fun (acc, left', newlow, lower') (d, l) ->
-	   let acc', (enf,alg,l',lower) = aux acc l in
-	   let l' =
-	     if enf then Universe.make l
-	     else l'
-	   in acc', (d, l') :: left',
-              lower_add l d newlow, lower_union lower lower')
-	  (acc, [], LMap.empty, LMap.empty) l
-        in
-        let not_lower (d,l) =
-        (* We're checking if (d,l) is already implied by the lower
-	  constraints on some level u. If it represents l < u (d is Lt
-	  or d is Le and i > 0, the i < 0 case is impossible due to
-	  invariants of Univ), and the lower constraints only have l <=
-	  u then it is not implied. *)
-          Univ.Universe.exists
-          (fun (l,i) ->
-             let d =
-               if i == 0 then d
-               else match d with
-                    | Le -> Lt
-                    | d -> d
-             in
-             try let d' = LMap.find l lower in
-                 (* If d is stronger than the already implied lower
-                  * constraints we must keep it. *)
-                 compare_constraint_type d d' > 0
-             with Not_found ->
-               (** No constraint existing on l *) true) l
-        in
-        let left = List.uniquize (List.filter not_lower left) in
-        (acc, left, LMap.union newlow lower)
-      with Not_found -> acc, [], LMap.empty
-    and right =
-      try Some (LMap.find u right)
-      with Not_found -> None
-    in
-    let instantiate_lbound lbound =
-      let alg = LSet.mem u algs in
-	if alg then
-	  (* u is algebraic: we instantiate it with its lower bound, if any,
-              or enforce the constraints if it is bounded from the top. *)
-          let lower = remove_lower lbound lower in
-	  instantiate_with_lbound u lbound lower true false acc
-	else (* u is non algebraic *)
-	  match Universe.level lbound with
-	  | Some l -> (* The lowerbound is directly a level *) 
-	     (* u is not algebraic but has no upper bounds,
-  	        we instantiate it with its lower bound if it is a 
-	        different level, otherwise we keep it. *)
-             let lower = LMap.remove l lower in
-	     if not (Level.equal l u) then
-	       (* Should check that u does not 
-  	          have upper constraints that are not already in right *)
-	       let acc' = remove_alg l acc in
-		 instantiate_with_lbound u lbound lower false false acc'
-	     else acc, (true, false, lbound, lower)
-	  | None ->
-	     try
-	       (* Another universe represents the same lower bound,
-                  we can share them with no harm. *)
-	       let can, lower = find_inst insts lbound in
-               let lower = LMap.remove can lower in
-	       instantiate_with_lbound u (Universe.make can) lower false false acc
-	  with Not_found -> 
-	    (* We set u as the canonical universe representing lbound *)
-	    instantiate_with_lbound u lbound lower false true acc
-    in
-    let acc' acc = 
-      match right with
-      | None -> acc
-      | Some cstrs -> 
-	let dangling = List.filter (fun (d, r) -> not (LMap.mem r us)) cstrs in
-	  if List.is_empty dangling then acc
-	  else
-	    let ((ctx', us, algs, insts, cstrs), (enf,_,inst,lower as b)) = acc in
-	    let cstrs' = List.fold_left (fun cstrs (d, r) -> 
-	      if d == Univ.Le then
-		enforce_leq inst (Universe.make r) cstrs
-	      else
-		try let lev = Option.get (Universe.level inst) in
-		      Constraint.add (lev, d, r) cstrs
-		with Option.IsNone -> failwith "")
-	      cstrs dangling
-	    in
-	      (ctx', us, algs, insts, cstrs'), b
-    in
-      if not (LSet.mem u ctx) then acc' (acc, (true, false, Universe.make u, lower))
-      else
-	let lbound = compute_lbound left in
-	  match lbound with
-	  | None -> (* Nothing to do *)
-	    acc' (acc, (true, false, Universe.make u, lower))
-	  | Some lbound ->
-	     try acc' (instantiate_lbound lbound) 
-	     with Failure _ -> acc' (acc, (true, false, Universe.make u, lower))
-  and aux (ctx', us, algs, seen, cstrs as acc) u =
-    try acc, LMap.find u seen 
-    with Not_found -> instance acc u
-  in
-    LMap.fold (fun u v (ctx', us, algs, seen, cstrs as acc) -> 
-      if v == None then fst (aux acc u)
-      else LSet.remove u ctx', us, LSet.remove u algs, seen, cstrs)
-      us (ctx, us, algs, lbounds, cstrs)
-
-let normalize_context_set g ctx us algs weak =
-  let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
-  let uf = UF.create () in
-  (** Keep the Prop/Set <= i constraints separate for minimization *)
-  let smallles, csts =
-    Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) ->
-        if d == Le then
-	  if Univ.Level.is_small l then
-	    if is_set_minimization () && LSet.mem r ctx then
-	      (Constraint.add cstr smallles, noneqs)
-	    else (smallles, noneqs)
-	  else if Level.is_small r then
-	    if Level.is_prop r then
-	      raise (Univ.UniverseInconsistency
-		       (Le,Universe.make l,Universe.make r,None))
-	    else (smallles, Constraint.add (l,Eq,r) noneqs)
-	  else (smallles, Constraint.add cstr noneqs)
-	else (smallles, Constraint.add cstr noneqs))
-    csts (Constraint.empty, Constraint.empty)
-  in
-  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 -> UGraph.add_universe v false g)
-			   ctx UGraph.initial_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 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 UGraph.add_universe r false g
-	     with UGraph.AlreadyDeclared -> g
-	   else g
-	 in g) csts g
-    in
-    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 ->
-      if d == Eq then (UF.union l r uf; noneqs)
-      else (* We ignore the trivial Prop/Set <= i constraints. *)
-	if d == Le && Univ.Level.is_small l then noneqs
-	else if Univ.Level.is_prop l && d == Lt && Univ.Level.is_set r
-	then noneqs
-	else Constraint.add cstr noneqs)
-      csts Constraint.empty
-  in
-  let noneqs = Constraint.union noneqs smallles in
-  let partition = UF.partition uf in
-  let flex x = LMap.mem x us in
-  let ctx, us, eqs = List.fold_left (fun (ctx, us, cstrs) s ->
-    let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in
-    (* Add equalities for globals which can't be merged anymore. *)
-    let cstrs = LSet.fold (fun g cst -> 
-      Constraint.add (canon, Univ.Eq, g) cst) global
-      cstrs 
-    in
-    (* Also add equalities for rigid variables *)
-    let cstrs = LSet.fold (fun g cst -> 
-      Constraint.add (canon, Univ.Eq, g) cst) rigid
-      cstrs
-    in
-    let canonu = Some (Universe.make canon) in
-    let us = LSet.fold (fun f -> LMap.add f canonu) flexible us in
-      (LSet.diff ctx flexible, us, cstrs))
-    (ctx, us, Constraint.empty) partition
-  in
-  (* Process weak constraints: when one side is flexible and the 2
-     universes are unrelated unify them. *)
-  let ctx, us, g = UPairSet.fold (fun (u,v) (ctx, us, g as acc) ->
-      let norm = let us = ref us in level_subst_of (normalize_univ_variable_opt_subst us) in
-      let u = norm u and v = norm v in
-      let set_to a b =
-        (LSet.remove a ctx,
-         LMap.add a (Some (Universe.make b)) us,
-         UGraph.enforce_constraint (a,Eq,b) g)
-      in
-      if UGraph.check_constraint g (u,Le,v) || UGraph.check_constraint g (v,Le,u)
-      then acc
-      else
-      if LMap.mem u us
-      then set_to u v
-      else if LMap.mem v us
-      then set_to v u
-      else acc)
-      weak (ctx, us, g)  in
-  (* Noneqs is now in canonical form w.r.t. equality constraints, 
-     and contains only inequality constraints. *)
-  let noneqs =
-    let us = ref us in
-    let norm = level_subst_of (normalize_univ_variable_opt_subst us) in
-    Constraint.fold (fun (u,d,v) noneqs ->
-        let u = norm u and v = norm v in
-        if d != Lt && Level.equal u v then noneqs
-        else Constraint.add (u,d,v) noneqs)
-      noneqs Constraint.empty
-  in
-  (* Compute the left and right set of flexible variables, constraints
-     mentionning other variables remain in noneqs. *)
-  let noneqs, ucstrsl, ucstrsr = 
-    Constraint.fold (fun (l,d,r as cstr) (noneq, ucstrsl, ucstrsr) -> 
-      let lus = LMap.mem l us and rus = LMap.mem r us in
-      let ucstrsl' = 
-	if lus then add_list_map l (d, r) ucstrsl
-	else ucstrsl
-      and ucstrsr' = 
-	add_list_map r (d, l) ucstrsr
-      in 
-      let noneqs = 
-	if lus || rus then noneq 
-	else Constraint.add cstr noneq
-      in (noneqs, ucstrsl', ucstrsr'))
-    noneqs (Constraint.empty, LMap.empty, LMap.empty)
-  in
-  (* Now we construct the instantiation of each variable. *)
-  let ctx', us, algs, inst, noneqs = 
-    minimize_univ_variables ctx us algs ucstrsr ucstrsl noneqs
-  in
-  let us = normalize_opt_subst us in
-    (us, algs), (ctx', Constraint.union noneqs eqs)
-
-(* let normalize_conkey = CProfile.declare_profile "normalize_context_set" *)
-(* let normalize_context_set a b c = CProfile.profile3 normalize_conkey normalize_context_set a b c *)
-
-let is_trivial_leq (l,d,r) =
-  Univ.Level.is_prop l && (d == Univ.Le || (d == Univ.Lt && Univ.Level.is_set r))
-
-(* Prop < i <-> Set+1 <= i <-> Set < i *)
-let translate_cstr (l,d,r as cstr) =
-  if Level.equal Level.prop l && d == Univ.Lt && not (Level.equal Level.set r) then
-    (Level.set, d, r)
-  else cstr
-
-let refresh_constraints univs (ctx, cstrs) =
-  let cstrs', univs' = 
-    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', UGraph.enforce_constraint c univs))
-      cstrs (Univ.Constraint.empty, univs)
-  in ((ctx, cstrs'), univs')
-
-
-(**********************************************************************)
-(* Tools for sort-polymorphic inductive types                         *)
-
-(* Miscellaneous functions to remove or test local univ assumed to
-   occur only in the le constraints *)
-
-(*
-   Solve a system of universe constraint of the form
-
-   u_s11, ..., u_s1p1, w1 <= u1
-   ...
-   u_sn1, ..., u_snpn, wn <= un
-
-where
-
-  - the ui (1 <= i <= n) are universe variables,
-  - the sjk select subsets of the ui for each equations,
-  - the wi are arbitrary complex universes that do not mention the ui.
-*)
+module Constraints = UnivProblem.Set
+type 'a constraint_accumulator = 'a UnivProblem.accumulator
+type 'a universe_constrained = 'a UnivProblem.constrained
+type 'a universe_constraint_function = 'a UnivProblem.constraint_function
+let subst_univs_universe_constraints = UnivProblem.Set.subst_univs
+let enforce_eq_instances_univs = UnivProblem.enforce_eq_instances_univs
+let to_constraints = UnivProblem.to_constraints
+let eq_constr_univs_infer_with = UnivProblem.eq_constr_univs_infer_with
 
-let is_direct_sort_constraint s v = match s with
-  | Some u -> univ_level_mem u v
-  | None -> false
+(** UnivMinim *)
+module UPairSet = UnivMinim.UPairSet
 
-let solve_constraints_system levels level_bounds level_min =
-  let open Univ in
-  let levels =
-    Array.mapi (fun i o ->
-      match o with
-      | Some u ->
-	(match Universe.level u with 
-	| Some u -> Some u 
-	| _ -> level_bounds.(i) <- Universe.sup level_bounds.(i) u; None)
-      | None -> None)
-      levels in
-  let v = Array.copy level_bounds in
-  let nind = Array.length v in
-  let clos = Array.map (fun _ -> Int.Set.empty) levels in
-  (* First compute the transitive closure of the levels dependencies *)
-  for i=0 to nind-1 do
-    for j=0 to nind-1 do
-      if not (Int.equal i j) && is_direct_sort_constraint levels.(j) v.(i) then
-	clos.(i) <- Int.Set.add j clos.(i);
-    done;
-  done;
-  let rec closure () = 
-    let continue = ref false in
-      Array.iteri (fun i deps -> 
-	let deps' = 
-	  Int.Set.fold (fun j acc -> Int.Set.union acc clos.(j)) deps deps
-	in 
-	  if Int.Set.equal deps deps' then ()
-	  else (clos.(i) <- deps'; continue := true))
-	clos;
-      if !continue then closure ()
-      else ()
-  in 
-  closure ();
-  for i=0 to nind-1 do
-    for j=0 to nind-1 do
-      if not (Int.equal i j) && Int.Set.mem j clos.(i) then
-	(v.(i) <- Universe.sup v.(i) level_bounds.(j));
-    done;
-  done;
-  v
+let normalize_context_set = UnivMinim.normalize_context_set
diff --git a/engine/universes.mli b/engine/universes.mli
index 4823c574..ad937471 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -8,227 +8,231 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Util
 open Names
 open Constr
 open Environ
 open Univ
 
-(** Unordered pairs of universe levels (ie (u,v) = (v,u)) *)
-module UPairSet : CSet.S with type elt = (Level.t * Level.t)
+(** ************************************** *)
+(** This entire module is deprecated. **** *)
+(** ************************************** *)
+[@@@ocaml.warning "-3"]
 
-val set_minimization : bool ref
-val is_set_minimization : unit -> bool
-
-(** Universes *)
+(** ****** Deprecated: moved to [UnivNames] *)
 
 val pr_with_global_universes : Level.t -> Pp.t
-val reference_of_level : Level.t -> Libnames.reference
+[@@ocaml.deprecated "Use [UnivNames.pr_with_global_universes]"]
+val reference_of_level : Level.t -> Libnames.qualid
+[@@ocaml.deprecated "Use [UnivNames.qualid_of_level]"]
 
-(** Global universe information outside the kernel, to handle
-    polymorphic universes in sections that have to be discharged. *)
 val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit
+[@@ocaml.deprecated "Use [UnivNames.add_global_universe]"]
 
 val is_polymorphic : Level.t -> bool
+[@@ocaml.deprecated "Use [UnivNames.is_polymorphic]"]
 
-(** Local universe name <-> level mapping *)
-
-type universe_binders = Univ.Level.t Names.Id.Map.t
+type universe_binders = UnivNames.universe_binders
+[@@ocaml.deprecated "Use [UnivNames.universe_binders]"]
 
 val empty_binders : universe_binders
+[@@ocaml.deprecated "Use [UnivNames.empty_binders]"]
 
 val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
+[@@ocaml.deprecated "Use [UnivNames.register_universe_binders]"]
 val universe_binders_of_global : Globnames.global_reference -> universe_binders
+[@@ocaml.deprecated "Use [UnivNames.universe_binders_of_global]"]
 
-type univ_name_list = Misctypes.lname list
-
-(** [universe_binders_with_opt_names ref u l]
+type univ_name_list = UnivNames.univ_name_list
+[@@ocaml.deprecated "Use [UnivNames.univ_name_list]"]
 
-    If [l] is [Some univs] return the universe binders naming the levels of [u] by [univs] (skipping Anonymous).
-    May error if the lengths mismatch.
-
-    Otherwise return [universe_binders_of_global ref]. *)
 val universe_binders_with_opt_names : Globnames.global_reference ->
   Univ.Level.t list -> univ_name_list option -> universe_binders
+[@@ocaml.deprecated "Use [UnivNames.universe_binders_with_opt_names]"]
 
-(** The global universe counter *)
-type universe_id = DirPath.t * int
+(** ****** Deprecated: moved to [UnivGen] *)
 
-val set_remote_new_univ_id : universe_id RemoteCounter.installer
+type universe_id = UnivGen.universe_id
+[@@ocaml.deprecated "Use [UnivGen.universe_id]"]
 
-(** Side-effecting functions creating new universe levels. *)
+val set_remote_new_univ_id : universe_id RemoteCounter.installer
+[@@ocaml.deprecated "Use [UnivGen.set_remote_new_univ_id]"]
 
 val new_univ_id : unit -> universe_id
+[@@ocaml.deprecated "Use [UnivGen.new_univ_id]"]
+
 val new_univ_level : unit -> Level.t
+[@@ocaml.deprecated "Use [UnivGen.new_univ_level]"]
+
 val new_univ : unit -> Universe.t
+[@@ocaml.deprecated "Use [UnivGen.new_univ]"]
+
 val new_Type : unit -> types
+[@@ocaml.deprecated "Use [UnivGen.new_Type]"]
+
 val new_Type_sort : unit -> Sorts.t
+[@@ocaml.deprecated "Use [UnivGen.new_Type_sort]"]
 
 val new_global_univ : unit -> Universe.t in_universe_context_set
-val new_sort_in_family : Sorts.family -> Sorts.t
-
-(** {6 Constraints for type inference}
-
-    When doing conversion of universes, not only do we have =/<= constraints but
-    also Lub constraints which correspond to unification of two levels which might
-    not be necessary if unfolding is performed.
-
-    UWeak constraints come from irrelevant universes in cumulative polymorphism.
-*)
-
-type universe_constraint =
-  | ULe of Universe.t * Universe.t
-  | UEq of Universe.t * Universe.t
-  | ULub of Level.t * Level.t
-  | UWeak of Level.t * Level.t
-
-module Constraints : sig
-  include Set.S with type elt = universe_constraint
-
-  val is_trivial : universe_constraint -> bool
-
-  val pr : t -> Pp.t
-end
-
-type universe_constraints = Constraints.t
-[@@ocaml.deprecated "Use Constraints.t"]
-
-type 'a constraint_accumulator = Constraints.t -> 'a -> 'a option
-type 'a universe_constrained = 'a * Constraints.t
-type 'a universe_constraint_function = 'a -> 'a -> Constraints.t -> Constraints.t
+[@@ocaml.deprecated "Use [UnivGen.new_global_univ]"]
 
-val subst_univs_universe_constraints : universe_subst_fn -> 
-  Constraints.t -> Constraints.t
-
-val enforce_eq_instances_univs : bool -> Instance.t universe_constraint_function
-
-(** With [force_weak] UWeak constraints are turned into equalities,
-   otherwise they're forgotten. *)
-val to_constraints : force_weak:bool -> UGraph.t -> Constraints.t -> Constraint.t
-
-(** [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
-    subterms of [m] and [n], arguments. *)
-val eq_constr_univs_infer_with :
-  (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
-  (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
-  UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option
-
-(** Build a fresh instance for a given context, its associated substitution and 
-    the instantiated constraints. *)
+val new_sort_in_family : Sorts.family -> Sorts.t
+[@@ocaml.deprecated "Use [UnivGen.new_sort_in_family]"]
 
-val fresh_instance_from_context : AUContext.t -> 
+val fresh_instance_from_context : AUContext.t ->
   Instance.t constrained
+[@@ocaml.deprecated "Use [UnivGen.fresh_instance_from_context]"]
 
 val fresh_instance_from : AUContext.t -> Instance.t option ->
   Instance.t in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.fresh_instance_from]"]
 
-val fresh_sort_in_family : env -> Sorts.family -> 
+val fresh_sort_in_family : Sorts.family ->
   Sorts.t in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.fresh_sort_in_family]"]
+
 val fresh_constant_instance : env -> Constant.t ->
   pconstant in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.fresh_constant_instance]"]
+
 val fresh_inductive_instance : env -> inductive ->
   pinductive in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.fresh_inductive_instance]"]
+
 val fresh_constructor_instance : env -> constructor ->
   pconstructor in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.fresh_constructor_instance]"]
 
-val fresh_global_instance : ?names:Univ.Instance.t -> env -> Globnames.global_reference -> 
+val fresh_global_instance : ?names:Univ.Instance.t -> env -> Globnames.global_reference ->
   constr in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.fresh_global_instance]"]
 
-val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> 
+val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr ->
   constr in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.fresh_global_or_constr_instance]"]
 
-(** Get fresh variables for the universe context.
-    Useful to make tactics that manipulate constrs in universe contexts polymorphic. *)
-val fresh_universe_context_set_instance : ContextSet.t -> 
+val fresh_universe_context_set_instance : ContextSet.t ->
   universe_level_subst * ContextSet.t
+[@@ocaml.deprecated "Use [UnivGen.fresh_universe_context_set_instance]"]
 
-(** Raises [Not_found] if not a global reference. *)
 val global_of_constr : constr -> Globnames.global_reference puniverses
+[@@ocaml.deprecated "Use [UnivGen.global_of_constr]"]
 
 val constr_of_global_univ : Globnames.global_reference puniverses -> constr
+[@@ocaml.deprecated "Use [UnivGen.constr_of_global_univ]"]
 
-val extend_context : 'a in_universe_context_set -> ContextSet.t -> 
+val extend_context : 'a in_universe_context_set -> ContextSet.t ->
   'a in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.extend_context]"]
 
-(** Simplification and pruning of constraints:
-    [normalize_context_set ctx us]
+val constr_of_global : Globnames.global_reference -> constr
+[@@ocaml.deprecated "Use [UnivGen.constr_of_global]"]
 
-    - Instantiate the variables in [us] with their most precise
-    universe levels respecting the constraints.
+val constr_of_reference : Globnames.global_reference -> constr
+[@@ocaml.deprecated "Use [UnivGen.constr_of_global]"]
 
-    - Normalizes the context [ctx] w.r.t. equality constraints, 
-    choosing a canonical universe in each equivalence class 
-    (a global one if there is one) and transitively saturate
-    the constraints w.r.t to the equalities. *)
+val type_of_global : Globnames.global_reference -> types in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.type_of_global]"]
 
-module UF : Unionfind.PartitionSig with type elt = Level.t
+(** ****** Deprecated: moved to [UnivSubst] *)
 
 val level_subst_of : universe_subst_fn -> universe_level_subst_fn
+[@@ocaml.deprecated "Use [UnivSubst.level_subst_of]"]
+
 val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t
+[@@ocaml.deprecated "Use [UnivSubst.subst_univs_constraints]"]
 
 val subst_univs_constr : universe_subst -> constr -> constr
+[@@ocaml.deprecated "Use [UnivSubst.subst_univs_constr]"]
 
-type universe_opt_subst = Universe.t option universe_map
+type universe_opt_subst = UnivSubst.universe_opt_subst
+[@@ocaml.deprecated "Use [UnivSubst.universe_opt_subst]"]
 
 val make_opt_subst : universe_opt_subst -> universe_subst_fn
+[@@ocaml.deprecated "Use [UnivSubst.make_opt_subst]"]
 
 val subst_opt_univs_constr : universe_opt_subst -> constr -> constr
+[@@ocaml.deprecated "Use [UnivSubst.subst_opt_univs_constr]"]
 
-val normalize_context_set : UGraph.t -> ContextSet.t ->
-  universe_opt_subst (* The defined and undefined variables *) ->
-  LSet.t (* univ variables that can be substituted by algebraics *) ->
-  UPairSet.t (* weak equality constraints *) ->
-  (universe_opt_subst * LSet.t) in_universe_context_set
+val normalize_univ_variables : universe_opt_subst ->
+  universe_opt_subst * LSet.t * universe_subst
+[@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variables]"]
 
-val normalize_univ_variables : universe_opt_subst -> 
-  universe_opt_subst * LSet.t * LSet.t * universe_subst
-
-val normalize_univ_variable : 
+val normalize_univ_variable :
   find:(Level.t -> Universe.t) ->
-  update:(Level.t -> Universe.t -> Universe.t) ->
   Level.t -> Universe.t
+[@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variable]"]
 
-val normalize_univ_variable_opt_subst : universe_opt_subst ref ->
+val normalize_univ_variable_opt_subst : universe_opt_subst ->
   (Level.t -> Universe.t)
+[@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variable_opt_subst]"]
 
-val normalize_univ_variable_subst : universe_subst ref ->
+val normalize_univ_variable_subst : universe_subst ->
   (Level.t -> Universe.t)
+[@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variable_subst]"]
 
-val normalize_universe_opt_subst : universe_opt_subst ref ->
+val normalize_universe_opt_subst : universe_opt_subst ->
   (Universe.t -> Universe.t)
+[@@ocaml.deprecated "Use [UnivSubst.normalize_universe_opt_subst]"]
 
-val normalize_universe_subst : universe_subst ref ->
+val normalize_universe_subst : universe_subst ->
   (Universe.t -> Universe.t)
+[@@ocaml.deprecated "Use [UnivSubst.normalize_universe_subst]"]
 
-(** Create a fresh global in the global environment, without side effects.
-    BEWARE: this raises an ANOMALY on polymorphic constants/inductives: 
-    the constraints should be properly added to an evd. 
-    See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for
-    the proper way to get a fresh copy of a global reference. *)
-val constr_of_global : Globnames.global_reference -> constr
+val nf_evars_and_universes_opt_subst : (existential -> constr option) ->
+  universe_opt_subst -> constr -> constr
+[@@ocaml.deprecated "Use [UnivSubst.nf_evars_and_universes_opt_subst]"]
 
-(** ** DEPRECATED ** synonym of [constr_of_global] *)
-val constr_of_reference : Globnames.global_reference -> constr
-[@@ocaml.deprecated "synonym of [constr_of_global]"]
+val pr_universe_opt_subst : universe_opt_subst -> Pp.t
+[@@ocaml.deprecated "Use [UnivSubst.pr_universe_opt_subst]"]
 
-(** Returns the type of the global reference, by creating a fresh instance of polymorphic 
-    references and computing their instantiated universe context. (side-effect on the
-    universe counter, use with care). *)
-val type_of_global : Globnames.global_reference -> types in_universe_context_set
+(** ****** Deprecated: moved to [UnivProblem] *)
 
-(** Full universes substitutions into terms *)
+type universe_constraint = UnivProblem.t =
+  | ULe of Universe.t * Universe.t [@ocaml.deprecated "Use [UnivProblem.ULe]"]
+  | UEq of Universe.t * Universe.t [@ocaml.deprecated "Use [UnivProblem.UEq]"]
+  | ULub of Level.t * Level.t [@ocaml.deprecated "Use [UnivProblem.ULub]"]
+  | UWeak of Level.t * Level.t [@ocaml.deprecated "Use [UnivProblem.UWeak]"]
+[@@ocaml.deprecated "Use [UnivProblem.t]"]
 
-val nf_evars_and_universes_opt_subst : (existential -> constr option) -> 
-  universe_opt_subst -> constr -> constr
+module Constraints = UnivProblem.Set
+[@@ocaml.deprecated "Use [UnivProblem.Set]"]
 
-val refresh_constraints : UGraph.t -> ContextSet.t -> ContextSet.t * UGraph.t
+type 'a constraint_accumulator = 'a UnivProblem.accumulator
+[@@ocaml.deprecated "Use [UnivProblem.accumulator]"]
+type 'a universe_constrained = 'a UnivProblem.constrained
+[@@ocaml.deprecated "Use [UnivProblem.constrained]"]
+type 'a universe_constraint_function = 'a UnivProblem.constraint_function
+[@@ocaml.deprecated "Use [UnivProblem.constraint_function]"]
 
-(** Pretty-printing *)
+val subst_univs_universe_constraints : universe_subst_fn ->
+  Constraints.t -> Constraints.t
+[@@ocaml.deprecated "Use [UnivProblem.Set.subst_univs]"]
 
-val pr_universe_opt_subst : universe_opt_subst -> Pp.t
+val enforce_eq_instances_univs : bool -> Instance.t universe_constraint_function
+[@@ocaml.deprecated "Use [UnivProblem.enforce_eq_instances_univs]"]
 
-(** {6 Support for template polymorphism } *)
+(** With [force_weak] UWeak constraints are turned into equalities,
+   otherwise they're forgotten. *)
+val to_constraints : force_weak:bool -> UGraph.t -> Constraints.t -> Constraint.t
+[@@ocaml.deprecated "Use [UnivProblem.to_constraints]"]
 
-val solve_constraints_system : Universe.t option array -> Universe.t array -> Universe.t array ->
-  Universe.t array
+(** [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
+    subterms of [m] and [n], arguments. *)
+val eq_constr_univs_infer_with :
+  (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
+  (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
+  UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option
+[@@ocaml.deprecated "Use [UnivProblem.eq_constr_univs_infer_with]"]
+
+(** ****** Deprecated: moved to [UnivMinim] *)
+
+module UPairSet = UnivMinim.UPairSet
+[@@ocaml.deprecated "Use [UnivMinim.UPairSet]"]
+
+val normalize_context_set : UGraph.t -> ContextSet.t ->
+  universe_opt_subst (* The defined and undefined variables *) ->
+  LSet.t (* univ variables that can be substituted by algebraics *) ->
+  UPairSet.t (* weak equality constraints *) ->
+  (universe_opt_subst * LSet.t) in_universe_context_set
+[@@ocaml.deprecated "Use [UnivMinim.normalize_context_set]"]
diff --git a/engine/univops.ml b/engine/univops.ml
index 76dbaa25..7f9672f8 100644
--- a/engine/univops.ml
+++ b/engine/univops.ml
@@ -11,103 +11,27 @@
 open Univ
 open Constr
 
-let universes_of_constr env c =
-  let open Declarations in
-  let rec aux s c = 
+let universes_of_constr c =
+  let rec aux s c =
     match kind c with
     | Const (c, u) ->
-      begin match (Environ.lookup_constant c env).const_universes with
-        | Polymorphic_const _ ->
           LSet.fold LSet.add (Instance.levels u) s
-        | Monomorphic_const (univs, _) ->
-          LSet.union s univs
-      end
     | Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
-      begin match (Environ.lookup_mind mind env).mind_universes with
-        | Cumulative_ind _ | Polymorphic_ind _ ->
           LSet.fold LSet.add (Instance.levels u) s
-        | Monomorphic_ind (univs,_) ->
-          LSet.union s univs
-      end
     | Sort u when not (Sorts.is_small u) ->
       let u = Sorts.univ_of_sort u in
       LSet.fold LSet.add (Universe.levels u) s
     | _ -> Constr.fold aux s c
   in aux LSet.empty c
 
-type graphnode = {
-  mutable up : constraint_type LMap.t;
-  mutable visited : bool
-}
-
-let merge_types d d0 =
-  match d, d0 with
-  | _, Lt | Lt, _ -> Lt
-  | Le, _ | _, Le -> Le
-  | Eq, Eq -> Eq
-
-let merge_up d b up =
-  let find = try Some (LMap.find b up) with Not_found -> None in
-  match find with
-  | Some d0 ->
-    let d = merge_types d d0 in
-    if d == d0 then up else LMap.add b d up
-  | None -> LMap.add b d up
-
-let add_up a d b graph =
-  let node, graph =
-    try LMap.find a graph, graph
-    with Not_found ->
-      let node = { up = LMap.empty; visited = false } in
-      node, LMap.add a node graph
-  in
-  node.up <- merge_up d b node.up;
-  graph
-
-(* for each node transitive close until you find a non removable, discard the rest *)
-let transitive_close removable graph =
-  let rec do_node a node =
-    if not node.visited
-    then
-      let keepup =
-        LMap.fold (fun b d keepup ->
-            if not (LSet.mem b removable)
-            then merge_up d b keepup
-            else
-              begin
-                match LMap.find b graph with
-                | bnode ->
-                  do_node b bnode;
-                  LMap.fold (fun k d' keepup ->
-                    merge_up (merge_types d d') k keepup)
-                    bnode.up keepup
-                | exception Not_found -> keepup
-              end
-          )
-          node.up LMap.empty
-      in
-      node.up <- keepup;
-      node.visited <- true
-  in
-  LMap.iter do_node graph
-
-let restrict_universe_context (univs,csts) keep =
-  let removable = LSet.diff univs keep in
-  let (csts, rem) =
-    Constraint.fold (fun (a,d,b as cst) (csts, rem) ->
-        if LSet.mem a removable || LSet.mem b removable
-        then (csts, add_up a d b rem)
-        else (Constraint.add cst csts, rem))
-      csts (Constraint.empty, LMap.empty)
-  in
-  transitive_close removable rem;
-  let csts =
-    LMap.fold (fun a node csts ->
-        if LSet.mem a removable
-        then csts
-        else
-          LMap.fold (fun b d csts -> Constraint.add (a,d,b) csts)
-            node.up csts)
-      rem csts
-  in
+let restrict_universe_context (univs, csts) keep =
+  let removed = LSet.diff univs keep in
+  if LSet.is_empty removed then univs, csts
+  else
+  let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in
+  let g = UGraph.empty_universes in
+  let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in
+  let g = UGraph.merge_constraints csts g in
+  let allkept = LSet.diff allunivs removed in
+  let csts = UGraph.constraints_for ~kept:allkept g in
   (LSet.inter univs keep, csts)
diff --git a/engine/univops.mli b/engine/univops.mli
index d1585414..57a53597 100644
--- a/engine/univops.mli
+++ b/engine/univops.mli
@@ -11,8 +11,11 @@
 open Constr
 open Univ
 
-(** The universes of monomorphic constants appear. *)
-val universes_of_constr : Environ.env -> constr -> LSet.t
+(** Return the set of all universes appearing in [constr]. *)
+val universes_of_constr : constr -> LSet.t
 
-(** Shrink a universe context to a restricted set of variables *)
+(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
+   the universes in [keep]. The constraints [csts] are adjusted so
+   that transitive constraints between remaining universes (those in
+   [keep] and those not in [univs]) are preserved. *)
 val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t