Merge PR #13415: Separate interning and pretyping of universes

Reviewed-by: mattam82

69 files changed, 616 insertions, 423 deletions

diff --git a/dev/ci/user-overlays/13415-SkySkimmer-intern-univs.sh b/dev/ci/user-overlays/13415-SkySkimmer-intern-univs.sh
new file mode 100644
index 0000000000..0bf806085e
--- /dev/null
+++ b/dev/ci/user-overlays/13415-SkySkimmer-intern-univs.sh
@@ -0,0 +1,8 @@
+if [ "$CI_PULL_REQUEST" = "13415" ] || [ "$CI_BRANCH" = "intern-univs" ]; then
+
+    overlay equations https://github.com/SkySkimmer/Coq-Equations intern-univs
+
+    overlay paramcoq https://github.com/SkySkimmer/paramcoq intern-univs
+
+    overlay elpi https://github.com/SkySkimmer/coq-elpi intern-univs
+fi
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index a9438c4aca..4faa12af79 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -27,6 +27,11 @@ let _ = Detyping.print_evar_arguments := true
 let _ = Detyping.print_universes := true
 let _ = Goptions.set_bool_option_value ["Printing";"Matching"] false
 
+let with_env_evm f x =
+  let env = Global.env() in
+  let sigma = Evd.from_env env in
+  f env sigma x
+
 (* std_ppcmds *)
 let pp   x = Pp.pp_with !Topfmt.std_ft x
 
@@ -75,7 +80,7 @@ let ppeconstr x = pp (pr_econstr x)
 let ppconstr_expr x = let sigma,env = get_current_context () in pp (Ppconstr.pr_constr_expr env sigma x)
 let ppsconstr x = ppconstr (Mod_subst.force_constr x)
 let ppconstr_univ x = Constrextern.with_universes ppconstr x
-let ppglob_constr = (fun x -> pp(pr_lglob_constr_env (Global.env()) x))
+let ppglob_constr = (fun x -> pp(with_env_evm pr_lglob_constr_env x))
 let pppattern = (fun x -> pp(envpp pr_constr_pattern_env x))
 let pptype = (fun x -> try pp(envpp (fun env evm t -> pr_ltype_env env evm t) x) with e -> pp (str (Printexc.to_string e)))
 let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
@@ -130,7 +135,7 @@ let rec pr_closure {idents=idents;typed=typed;untyped=untyped} =
 and pr_closed_glob_constr_idmap x =
   pridmap (fun _ -> pr_closed_glob_constr) x
 and pr_closed_glob_constr {closure=closure;term=term} =
-  pr_closure closure ++ (pr_lglob_constr_env Global.(env ())) term
+  pr_closure closure ++ with_env_evm pr_lglob_constr_env term
 
 let ppclosure x = pp (pr_closure x)
 let ppclosedglobconstr x = pp (pr_closed_glob_constr x)
@@ -212,7 +217,7 @@ let pproof p = pp(Proof.pr_proof p)
 let ppuni u = pp(Universe.pr u)
 let ppuni_level u = pp (Level.pr u)
 
-let prlev = UnivNames.pr_with_global_universes
+let prlev = UnivNames.pr_with_global_universes Id.Map.empty
 let ppuniverse_set l = pp (LSet.pr prlev l)
 let ppuniverse_instance l = pp (Instance.pr prlev l)
 let ppuniverse_context l = pp (pr_universe_context prlev l)
diff --git a/doc/changelog/03-notations/13415-intern-univs.rst b/doc/changelog/03-notations/13415-intern-univs.rst
new file mode 100644
index 0000000000..e9f51461e5
--- /dev/null
+++ b/doc/changelog/03-notations/13415-intern-univs.rst
@@ -0,0 +1,5 @@
+- **Fixed:** Notations understand universe names without getting
+  confused by different imported modules between declaration and use
+  locations (`#13415 <https://github.com/coq/coq/pull/13415>`_, fixes
+  `#13303 <https://github.com/coq/coq/issues/13303>`_, by Gaëtan
+  Gilbert).
diff --git a/engine/uState.ml b/engine/uState.ml
index 103b552d86..0c994dfea0 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -341,12 +341,16 @@ let constrain_variables diff uctx =
   in
   { uctx with local = (univs, local); univ_variables = vars }
 
-let qualid_of_level uctx =
+let id_of_level uctx l =
+  try Some (Option.get (LMap.find l (snd uctx.names)).uname)
+  with Not_found | Option.IsNone ->
+    None
+
+let qualid_of_level uctx l =
   let map, map_rev = uctx.names in
-    fun l ->
-      try Some (Libnames.qualid_of_ident (Option.get (LMap.find l map_rev).uname))
-      with Not_found | Option.IsNone ->
-        UnivNames.qualid_of_level l
+  try Some (Libnames.qualid_of_ident (Option.get (LMap.find l map_rev).uname))
+  with Not_found | Option.IsNone ->
+    UnivNames.qualid_of_level map l
 
 let pr_uctx_level uctx l =
   match qualid_of_level uctx l with
diff --git a/engine/uState.mli b/engine/uState.mli
index bd3aac0d8b..442c29180c 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -209,4 +209,7 @@ val update_sigma_univs : t -> UGraph.t -> t
 val pr_uctx_level : t -> Univ.Level.t -> Pp.t
 val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid option
 
+(** Only looks in the local names, not in the nametab. *)
+val id_of_level : t -> Univ.Level.t -> Id.t option
+
 val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t
diff --git a/engine/univNames.ml b/engine/univNames.ml
index 2e15558db2..f5542cc0f7 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -12,15 +12,15 @@ open Names
 open Univ
 
 
-let qualid_of_level l =
+let qualid_of_level ctx l =
   match Level.name l with
   | Some qid  ->
-    (try Some (Nametab.shortest_qualid_of_universe qid)
+    (try Some (Nametab.shortest_qualid_of_universe (Id.Map.domain ctx) qid)
      with Not_found -> None)
   | None -> None
 
-let pr_with_global_universes l =
-  match qualid_of_level l with
+let pr_with_global_universes ctx l =
+  match qualid_of_level ctx l with
   | Some qid  -> Libnames.pr_qualid qid
   | None -> Level.pr l
 
diff --git a/engine/univNames.mli b/engine/univNames.mli
index 5f69d199b3..875c043032 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -10,9 +10,6 @@
 
 open Univ
 
-val pr_with_global_universes : Level.t -> Pp.t
-val qualid_of_level : Level.t -> Libnames.qualid option
-
 (** Local universe name <-> level mapping *)
 
 type universe_binders = Univ.Level.t Names.Id.Map.t
@@ -20,3 +17,6 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
 val empty_binders : universe_binders
 
 type univ_name_list = Names.lname list
+
+val pr_with_global_universes : universe_binders -> Level.t -> Pp.t
+val qualid_of_level : universe_binders -> Level.t -> Libnames.qualid option
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index b3f06faa1c..b14c325f69 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -13,10 +13,23 @@ open Libnames
 
 (** {6 Concrete syntax for terms } *)
 
-(** [constr_expr] is the abstract syntax tree produced by the parser *)
-type universe_decl_expr = (lident list, Glob_term.glob_constraint list) UState.gen_universe_decl
+(** Universes *)
+type sort_name_expr =
+  | CSProp | CProp | CSet
+  | CType of qualid
+  | CRawType of Univ.Level.t (** Universes like "foo.1" have no qualid form *)
+
+type univ_level_expr  = sort_name_expr Glob_term.glob_sort_gen
+type sort_expr = (sort_name_expr * int) list Glob_term.glob_sort_gen
+
+type instance_expr = univ_level_expr list
+
+(** Constraints don't have anonymous universes *)
+type univ_constraint_expr = sort_name_expr * Univ.constraint_type * sort_name_expr
+
+type universe_decl_expr = (lident list, univ_constraint_expr list) UState.gen_universe_decl
 type cumul_univ_decl_expr =
-  ((lident * Univ.Variance.t option) list, Glob_term.glob_constraint list) UState.gen_universe_decl
+  ((lident * Univ.Variance.t option) list, univ_constraint_expr list) UState.gen_universe_decl
 
 type ident_decl = lident * universe_decl_expr option
 type cumul_ident_decl = lident * cumul_univ_decl_expr option
@@ -64,8 +77,7 @@ type prim_token =
   | Number of NumTok.Signed.t
   | String of string
 
-type instance_expr = Glob_term.glob_level list
-
+(** [constr_expr] is the abstract syntax tree produced by the parser *)
 type cases_pattern_expr_r =
   | CPatAlias of cases_pattern_expr * lname
   | CPatCstr  of qualid
@@ -114,7 +126,7 @@ and constr_expr_r =
   | CHole   of Evar_kinds.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option
   | CPatVar of Pattern.patvar
   | CEvar   of Glob_term.existential_name CAst.t * (lident * constr_expr) list
-  | CSort   of Glob_term.glob_sort
+  | CSort   of sort_expr
   | CCast   of constr_expr * constr_expr Glob_term.cast_type
   | CNotation of notation_with_optional_scope option * notation * constr_notation_substitution
   | CGeneralization of Glob_term.binding_kind * abstraction_kind option * constr_expr
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index a60dc11b57..f02874253e 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -18,6 +18,25 @@ open Glob_term
 open Notation
 open Constrexpr
 
+(***********)
+(* Universes *)
+
+let sort_name_expr_eq c1 c2 = match c1, c2 with
+  | CSProp, CSProp
+  | CProp, CProp
+  | CSet, CSet -> true
+  | CType q1, CType q2 -> Libnames.qualid_eq q1 q2
+  | CRawType u1, CRawType u2 -> Univ.Level.equal u1 u2
+  | (CSProp|CProp|CSet|CType _|CRawType _), _ -> false
+
+let univ_level_expr_eq u1 u2 =
+  Glob_ops.glob_sort_gen_eq sort_name_expr_eq u1 u2
+
+let sort_expr_eq u1 u2 =
+  Glob_ops.glob_sort_gen_eq
+    (List.equal (fun (x,m) (y,n) -> sort_name_expr_eq x y && Int.equal m n))
+    u1 u2
+
 (***********************)
 (* For binders parsing *)
 
@@ -59,13 +78,11 @@ let explicitation_eq ex1 ex2 = match ex1, ex2 with
   Id.equal id1 id2
 | _ -> false
 
-let eq_ast f { CAst.v = x } { CAst.v = y } = f x y
-
 let rec cases_pattern_expr_eq p1 p2 =
   if CAst.(p1.v == p2.v) then true
   else match CAst.(p1.v, p2.v) with
   | CPatAlias(a1,i1), CPatAlias(a2,i2) ->
-      eq_ast Name.equal i1 i2 && cases_pattern_expr_eq a1 a2
+      CAst.eq Name.equal i1 i2 && cases_pattern_expr_eq a1 a2
   | CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) ->
       qualid_eq c1 c2 &&
       Option.equal (List.equal cases_pattern_expr_eq) a1 a2 &&
@@ -108,10 +125,10 @@ let rec constr_expr_eq e1 e2 =
   else match CAst.(e1.v, e2.v) with
     | CRef (r1,u1), CRef (r2,u2) -> qualid_eq r1 r2 && eq_universes u1 u2
     | CFix(id1,fl1), CFix(id2,fl2) ->
-      eq_ast Id.equal id1 id2 &&
+      lident_eq id1 id2 &&
       List.equal fix_expr_eq fl1 fl2
     | CCoFix(id1,fl1), CCoFix(id2,fl2) ->
-      eq_ast Id.equal id1 id2 &&
+      lident_eq id1 id2 &&
       List.equal cofix_expr_eq fl1 fl2
     | CProdN(bl1,a1), CProdN(bl2,a2) ->
       List.equal local_binder_eq bl1 bl2 &&
@@ -120,7 +137,7 @@ let rec constr_expr_eq e1 e2 =
       List.equal local_binder_eq bl1 bl2 &&
       constr_expr_eq a1 a2
     | CLetIn(na1,a1,t1,b1), CLetIn(na2,a2,t2,b2) ->
-      eq_ast Name.equal na1 na2 &&
+      CAst.eq Name.equal na1 na2 &&
       constr_expr_eq a1 a2 &&
       Option.equal constr_expr_eq t1 t2 &&
       constr_expr_eq b1 b2
@@ -144,14 +161,14 @@ let rec constr_expr_eq e1 e2 =
       List.equal case_expr_eq a1 a2 &&
       List.equal branch_expr_eq brl1 brl2
     | CLetTuple (n1, (m1, e1), t1, b1), CLetTuple (n2, (m2, e2), t2, b2) ->
-      List.equal (eq_ast Name.equal) n1 n2 &&
-      Option.equal (eq_ast Name.equal) m1 m2 &&
+      List.equal (CAst.eq Name.equal) n1 n2 &&
+      Option.equal (CAst.eq Name.equal) m1 m2 &&
       Option.equal constr_expr_eq e1 e2 &&
       constr_expr_eq t1 t2 &&
       constr_expr_eq b1 b2
     | CIf (e1, (n1, r1), t1, f1), CIf (e2, (n2, r2), t2, f2) ->
       constr_expr_eq e1 e2 &&
-      Option.equal (eq_ast Name.equal) n1 n2 &&
+      Option.equal (CAst.eq Name.equal) n1 n2 &&
       Option.equal constr_expr_eq r1 r2 &&
       constr_expr_eq t1 t2 &&
       constr_expr_eq f1 f2
@@ -161,7 +178,7 @@ let rec constr_expr_eq e1 e2 =
     | CEvar (id1, c1), CEvar (id2, c2) ->
       Id.equal id1.CAst.v id2.CAst.v && List.equal instance_eq c1 c2
     | CSort s1, CSort s2 ->
-      Glob_ops.glob_sort_eq s1 s2
+      sort_expr_eq s1 s2
     | CCast(t1,c1), CCast(t2,c2) ->
       constr_expr_eq t1 t2 && cast_expr_eq c1 c2
     | CNotation(inscope1, n1, s1), CNotation(inscope2, n2, s2) ->
@@ -187,12 +204,12 @@ let rec constr_expr_eq e1 e2 =
      | CGeneralization _ | CDelimiters _ | CArray _), _ -> false
 
 and args_eq (a1,e1) (a2,e2) =
-  Option.equal (eq_ast explicitation_eq) e1 e2 &&
+  Option.equal (CAst.eq explicitation_eq) e1 e2 &&
   constr_expr_eq a1 a2
 
 and case_expr_eq (e1, n1, p1) (e2, n2, p2) =
   constr_expr_eq e1 e2 &&
-  Option.equal (eq_ast Name.equal) n1 n2 &&
+  Option.equal (CAst.eq Name.equal) n1 n2 &&
   Option.equal cases_pattern_expr_eq p1 p2
 
 and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} =
@@ -200,35 +217,35 @@ and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} =
   constr_expr_eq e1 e2
 
 and fix_expr_eq (id1,r1,bl1,a1,b1) (id2,r2,bl2,a2,b2) =
-  (eq_ast Id.equal id1 id2) &&
+  (lident_eq id1 id2) &&
   Option.equal recursion_order_expr_eq r1 r2 &&
   List.equal local_binder_eq bl1 bl2 &&
   constr_expr_eq a1 a2 &&
   constr_expr_eq b1 b2
 
 and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) =
-  (eq_ast Id.equal id1 id2) &&
+  (lident_eq id1 id2) &&
   List.equal local_binder_eq bl1 bl2 &&
   constr_expr_eq a1 a2 &&
   constr_expr_eq b1 b2
 
 and recursion_order_expr_eq_r r1 r2 = match r1, r2 with
-  | CStructRec i1, CStructRec i2 -> eq_ast Id.equal i1 i2
+  | CStructRec i1, CStructRec i2 -> lident_eq i1 i2
   | CWfRec (i1,e1), CWfRec (i2,e2) ->
     constr_expr_eq e1 e2
   | CMeasureRec (i1, e1, o1), CMeasureRec (i2, e2, o2) ->
-    Option.equal (eq_ast Id.equal) i1 i2 &&
+    Option.equal lident_eq i1 i2 &&
     constr_expr_eq e1 e2 && Option.equal constr_expr_eq o1 o2
   | _ -> false
 
-and recursion_order_expr_eq r1 r2 = eq_ast recursion_order_expr_eq_r r1 r2
+and recursion_order_expr_eq r1 r2 = CAst.eq recursion_order_expr_eq_r r1 r2
 
 and local_binder_eq l1 l2 = match l1, l2 with
   | CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) ->
-    eq_ast Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2
+    CAst.eq Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2
   | CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) ->
     (* Don't care about the [binder_kind] *)
-    List.equal (eq_ast Name.equal) n1 n2 && constr_expr_eq e1 e2
+    List.equal (CAst.eq Name.equal) n1 n2 && constr_expr_eq e1 e2
   | _ -> false
 
 and constr_notation_substitution_eq (e1, el1, b1, bl1) (e2, el2, b2, bl2) =
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index dfa51918d1..ffa7c8ec10 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -16,6 +16,10 @@ open Constrexpr
 
 (** {6 Equalities on [constr_expr] related types} *)
 
+val sort_name_expr_eq : sort_name_expr -> sort_name_expr -> bool
+val univ_level_expr_eq : univ_level_expr -> univ_level_expr -> bool
+val sort_expr_eq : sort_expr -> sort_expr -> bool
+
 val explicitation_eq : explicitation -> explicitation -> bool
 (** Equality on [explicitation]. *)
 
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 378adb566c..3969c7ea1f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -923,22 +923,44 @@ let extern_float f scopes =
 (**********************************************************************)
 (* mapping glob_constr to constr_expr                                    *)
 
-let extern_glob_sort = function
+type extern_env = Id.Set.t * UnivNames.universe_binders
+let extern_env env sigma = vars_of_env env, Evd.universe_binders sigma
+let empty_extern_env = Id.Set.empty, Id.Map.empty
+
+let extern_glob_sort_name uvars = function
+  | GSProp -> CSProp
+  | GProp -> CProp
+  | GSet -> CSet
+  | GLocalUniv u -> CType (qualid_of_lident u)
+  | GRawUniv u -> CRawType u
+  | GUniv u -> begin match UnivNames.qualid_of_level uvars u with
+      | Some qid -> CType qid
+      | None -> CRawType u
+    end
+
+let extern_glob_sort uvars =
+  map_glob_sort_gen (List.map (on_fst (extern_glob_sort_name uvars)))
+
+(** wrapper to handle print_universes: don't forget small univs *)
+let extern_glob_sort uvars = function
   (* In case we print a glob_constr w/o having passed through detyping *)
-  | UNamed [(GSProp,0) | (GProp,0) | (GSet,0)] as u -> u
+  | UNamed [(GSProp,0) | (GProp,0) | (GSet,0)] as u -> extern_glob_sort uvars u
   | UNamed _ when not !print_universes -> UAnonymous {rigid=true}
-  | UNamed _ | UAnonymous _ as u -> u
+  | UNamed _ | UAnonymous _ as u -> extern_glob_sort uvars u
 
-let extern_universes = function
-  | Some _ as l when !print_universes -> l
+let extern_instance uvars = function
+  | Some l when !print_universes ->
+    Some (List.map (map_glob_sort_gen (extern_glob_sort_name uvars)) l)
   | _ -> None
 
-let extern_ref vars ref us =
+let extern_ref (vars,uvars) ref us =
   extern_global (select_stronger_impargs (implicits_of_global ref))
-    (extern_reference vars ref) (extern_universes us)
+    (extern_reference vars ref) (extern_instance uvars us)
 
 let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None)
 
+let add_vname (vars,uvars) na = add_vname vars na, uvars
+
 let rec extern inctx ?impargs scopes vars r =
   match remove_one_coercion inctx (flatten_application r) with
   | Some (nargs,inctx,r') ->
@@ -995,7 +1017,7 @@ let rec extern inctx ?impargs scopes vars r =
              (* Otherwise... *)
                extern_applied_ref inctx
                  (select_stronger_impargs (implicits_of_global ref))
-                 (ref,extern_reference ?loc vars ref) (extern_universes us) args)
+                 (ref,extern_reference ?loc (fst vars) ref) (extern_instance (snd vars) us) args)
          | _ ->
              let args = List.map (fun c -> (sub_extern true scopes vars c,None)) args in
              let head = sub_extern false scopes vars f in
@@ -1015,7 +1037,8 @@ let rec extern inctx ?impargs scopes vars r =
   | GCases (sty,rtntypopt,tml,eqns) ->
     let vars' =
       List.fold_right (Name.fold_right Id.Set.add)
-        (cases_predicate_names tml) vars in
+        (cases_predicate_names tml) (fst vars) in
+    let vars' = vars', snd vars in
     let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in
     let tml = List.map (fun (tm,(na,x)) ->
                  let na' = match na, DAst.get tm with
@@ -1035,7 +1058,7 @@ let rec extern inctx ?impargs scopes vars r =
                   Option.map (fun {CAst.loc;v=(ind,nal)} ->
                               let args = List.map (fun x -> DAst.make @@ PatVar x) nal in
                               let fullargs = add_cpatt_for_params ind args in
-                              extern_ind_pattern_in_scope scopes vars ind fullargs
+                              extern_ind_pattern_in_scope scopes (fst vars) ind fullargs
                              ) x))
                 tml
     in
@@ -1058,7 +1081,7 @@ let rec extern inctx ?impargs scopes vars r =
         sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2)
 
   | GRec (fk,idv,blv,tyv,bv) ->
-      let vars' = Array.fold_right Id.Set.add idv vars in
+      let vars' = on_fst (Array.fold_right Id.Set.add idv) vars in
       (match fk with
          | GFix (nv,n) ->
              let listdecl =
@@ -1066,8 +1089,8 @@ let rec extern inctx ?impargs scopes vars r =
                  let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in
                  let bl = List.map (extended_glob_local_binder_of_decl ?loc) bl in
                  let (assums,ids,bl) = extern_local_binder scopes vars bl in
-                 let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in
-                 let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in
+                 let vars0 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars in
+                 let vars1 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars' in
                  let n =
                    match nv.(i) with
                    | None -> None
@@ -1082,14 +1105,14 @@ let rec extern inctx ?impargs scopes vars r =
                Array.mapi (fun i fi ->
                  let bl = List.map (extended_glob_local_binder_of_decl ?loc) blv.(i) in
                  let (_,ids,bl) = extern_local_binder scopes vars bl in
-                 let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in
-                 let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in
+                 let vars0 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars in
+                 let vars1 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars' in
                  ((CAst.make fi),bl,extern_typ scopes vars0 tyv.(i),
                   sub_extern true scopes vars1 bv.(i))) idv
              in
              CCoFix (CAst.(make ?loc idv.(n)),Array.to_list listdecl))
 
-  | GSort s -> CSort (extern_glob_sort s)
+  | GSort s -> CSort (extern_glob_sort (snd vars) s)
 
   | GHole (e,naming,_) -> CHole (Some e, naming, None) (* TODO: extern tactics. *)
 
@@ -1105,7 +1128,7 @@ let rec extern inctx ?impargs scopes vars r =
   | GFloat f -> extern_float f (snd scopes)
 
   | GArray(u,t,def,ty) ->
-    CArray(extern_universes u,Array.map (extern inctx scopes vars) t, extern inctx scopes vars def, extern_typ scopes vars ty)
+    CArray(extern_instance (snd vars) u,Array.map (extern inctx scopes vars) t, extern inctx scopes vars def, extern_typ scopes vars ty)
 
   in insert_entry_coercion coercion (CAst.make ?loc c)
 
@@ -1127,7 +1150,7 @@ and factorize_prod ?impargs scopes vars na bk t c =
       let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in
       let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in
       let b = extern_typ scopes vars b in
-      let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in
+      let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes (fst vars)) disjpat) in
       let binder = CLocalPattern p in
       (match b.v with
       | CProdN (bl,b) -> CProdN (binder::bl,b)
@@ -1168,7 +1191,7 @@ and factorize_lambda inctx scopes vars na bk t c =
       let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in
       let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in
       let b = sub_extern inctx scopes vars b in
-      let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in
+      let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes (fst vars)) disjpat) in
       let binder = CLocalPattern p in
       (match b.v with
       | CLambdaN (bl,b) -> CLambdaN (binder::bl,b)
@@ -1196,7 +1219,7 @@ and extern_local_binder scopes vars = function
     match DAst.get b with
     | GLocalDef (na,bk,bd,ty) ->
       let (assums,ids,l) =
-        extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l in
+        extern_local_binder scopes (on_fst (Name.fold_right Id.Set.add na) vars) l in
       (assums,na::ids,
        CLocalDef(CAst.make na, extern false scopes vars bd,
                    Option.map (extern_typ scopes vars) ty) :: l)
@@ -1204,7 +1227,7 @@ and extern_local_binder scopes vars = function
     | GLocalAssum (na,bk,ty) ->
       let implicit_type = is_reserved_type na ty in
       let ty = extern_typ scopes vars ty in
-      (match extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l with
+      (match extern_local_binder scopes (on_fst (Name.fold_right Id.Set.add na) vars) l with
           (assums,ids,CLocalAssum(nal,k,ty')::l)
             when (constr_expr_eq ty ty' || implicit_type && constr_expr_eq ty' hole) &&
               match na with Name id -> not (occur_var_constr_expr id ty')
@@ -1219,7 +1242,7 @@ and extern_local_binder scopes vars = function
     | GLocalPattern ((p,_),_,bk,ty) ->
       let ty =
         if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in
-      let p = mkCPatOr (List.map (extern_cases_pattern vars) p) in
+      let p = mkCPatOr (List.map (extern_cases_pattern (fst vars)) p) in
       let (assums,ids,l) = extern_local_binder scopes vars l in
       let p = match ty with
         | None -> p
@@ -1227,7 +1250,7 @@ and extern_local_binder scopes vars = function
       (assums,ids, CLocalPattern p :: l)
 
 and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} =
-  let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in
+  let pll = List.map (List.map (extern_cases_pattern_in_scope scopes (fst vars))) pll in
   make ?loc (pll,extern inctx scopes vars c)
 
 and extern_notations inctx scopes vars nargs t =
@@ -1277,6 +1300,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
             end
           | AppBoundedNotation _ -> raise No_match in
         (* Try matching ... *)
+        let vars, uvars = vars in
         let terms,termlists,binders,binderlists =
           match_notation_constr ~print_univ:(!print_universes) t ~vars pat in
         (* Try availability of interpretation ... *)
@@ -1300,35 +1324,43 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
                   let l =
                     List.map (fun ((vars,c),(subentry,(scopt,scl))) ->
                       extern (* assuming no overloading: *) true
-                        (subentry,(scopt,scl@scopes')) vars c)
-                      terms in
+                        (subentry,(scopt,scl@scopes')) (vars,uvars) c)
+                      terms
+                  in
                   let ll =
                     List.map (fun ((vars,l),(subentry,(scopt,scl))) ->
-                      List.map (extern true (subentry,(scopt,scl@scopes')) vars) l)
-                      termlists in
+                      List.map (extern true (subentry,(scopt,scl@scopes')) (vars,uvars)) l)
+                      termlists
+                  in
                   let bl =
                     List.map (fun ((vars,bl),(subentry,(scopt,scl))) ->
-                      (mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl)),
-                      Explicit)
-                      binders in
+                        (mkCPatOr (List.map
+                                     (extern_cases_pattern_in_scope
+                                        (subentry,(scopt,scl@scopes')) vars)
+                                     bl)),
+                        Explicit)
+                      binders
+                  in
                   let bll =
                     List.map (fun ((vars,bl),(subentry,(scopt,scl))) ->
-                      pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl))
-                      binderlists in
+                      pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) (vars,uvars) bl))
+                      binderlists
+                  in
                   let c = make_notation loc specific_ntn (l,ll,bl,bll) in
                   let c = insert_entry_coercion coercion (insert_delimiters c key) in
                   let args = fill_arg_scopes args argsscopes allscopes in
-                  let args = extern_args (extern true) vars args in
+                  let args = extern_args (extern true) (vars,uvars) args in
                   CAst.make ?loc @@ extern_applied_notation inctx nallargs argsimpls c args)
           | SynDefRule kn ->
               let l =
                 List.map (fun ((vars,c),(subentry,(scopt,scl))) ->
-                  extern true (subentry,(scopt,scl@snd scopes)) vars c)
-                  terms in
+                  extern true (subentry,(scopt,scl@snd scopes)) (vars,uvars) c)
+                  terms
+              in
               let cf = Nametab.shortest_qualid_of_syndef ?loc vars kn in
               let a = CRef (cf,None) in
               let args = fill_arg_scopes args argsscopes allscopes in
-              let args = extern_args (extern true) vars args in
+              let args = extern_args (extern true) (vars,uvars) args in
               let c = CAst.make ?loc @@ extern_applied_syntactic_definition inctx nallargs argsimpls (a,cf) l args in
               if isCRef_no_univ c.CAst.v && entry_has_global custom then c
              else match availability_of_entry_coercion custom InConstrEntrySomeLevel with
@@ -1348,7 +1380,7 @@ let extern_glob_type ?impargs vars c =
 
 let extern_constr ?lax ?(inctx=false) ?scope env sigma t =
   let r = Detyping.detype Detyping.Later ?lax false Id.Set.empty env sigma t in
-  let vars = vars_of_env env in
+  let vars = extern_env env sigma in
   extern inctx (InConstrEntrySomeLevel,(scope,[])) vars r
 
 let extern_constr_in_scope ?lax ?inctx scope env sigma t =
@@ -1364,16 +1396,16 @@ let extern_type ?lax ?(goal_concl_style=false) env sigma ?impargs t =
   (* consideration; see namegen.ml for further details *)
   let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in
   let r = Detyping.detype Detyping.Later ?lax goal_concl_style avoid env sigma t in
-  extern_glob_type ?impargs (vars_of_env env) r
+  extern_glob_type ?impargs (extern_env env sigma) r
 
-let extern_sort sigma s = extern_glob_sort (detype_sort sigma s)
+let extern_sort sigma s = extern_glob_sort (Evd.universe_binders sigma) (detype_sort sigma s)
 
 let extern_closed_glob ?lax ?(goal_concl_style=false) ?(inctx=false) ?scope env sigma t =
   let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in
   let r =
     Detyping.detype_closed_glob ?lax goal_concl_style avoid env sigma t
   in
-  let vars = vars_of_env env in
+  let vars = extern_env env sigma in
   extern inctx (InConstrEntrySomeLevel,(scope,[])) vars r
 
 (******************************************************************)
@@ -1491,10 +1523,13 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
     GArray (None, Array.map glob_of t, glob_of def, glob_of ty)
 
 let extern_constr_pattern env sigma pat =
-  extern true (InConstrEntrySomeLevel,(None,[])) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat)
+  extern true (InConstrEntrySomeLevel,(None,[]))
+    (* XXX no vars? *)
+    (Id.Set.empty, Evd.universe_binders sigma)
+    (glob_of_pat Id.Set.empty env sigma pat)
 
 let extern_rel_context where env sigma sign =
   let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in
-  let vars = vars_of_env env in
+  let vars = extern_env env sigma in
   let a = List.map (extended_glob_local_binder_of_decl) a in
   pi3 (extern_local_binder (InConstrEntrySomeLevel,(None,[])) vars a)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index f85e49d2df..298b52f0be 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -23,9 +23,12 @@ open Ltac_pretype
 (** Translation of pattern, cases pattern, glob_constr and term into syntax
    trees for printing *)
 
+type extern_env = Id.Set.t * UnivNames.universe_binders
+val extern_env : env -> Evd.evar_map -> extern_env
+
 val extern_cases_pattern : Id.Set.t -> 'a cases_pattern_g -> cases_pattern_expr
-val extern_glob_constr : Id.Set.t -> 'a glob_constr_g -> constr_expr
-val extern_glob_type : ?impargs:Glob_term.binding_kind list -> Id.Set.t -> 'a glob_constr_g -> constr_expr
+val extern_glob_constr : extern_env -> 'a glob_constr_g -> constr_expr
+val extern_glob_type : ?impargs:Glob_term.binding_kind list -> extern_env -> 'a glob_constr_g -> constr_expr
 val extern_constr_pattern : names_context -> Evd.evar_map ->
   constr_pattern -> constr_expr
 val extern_closed_glob : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name ->
@@ -43,7 +46,7 @@ val extern_constr_in_scope : ?lax:bool -> ?inctx:bool -> scope_name ->
   env -> Evd.evar_map -> constr -> constr_expr
 val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
 val extern_type : ?lax:bool -> ?goal_concl_style:bool -> env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> types -> constr_expr
-val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort
+val extern_sort : Evd.evar_map -> Sorts.t -> sort_expr
 val extern_rel_context : constr option -> env -> Evd.evar_map ->
   rel_context -> local_binder_expr list
 
@@ -96,3 +99,6 @@ val toggle_scope_printing :
 
 val toggle_notation_printing :
   ?scope:Notation_term.scope_name -> notation:Constrexpr.notation -> activate:bool -> unit
+
+(** Probably shouldn't be used *)
+val empty_extern_env : extern_env
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 0645636255..cf2f333596 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -254,9 +254,12 @@ let contract_curly_brackets_pat ntn (l,ll) =
   (* side effect; don't inline *)
   (InConstrEntry,!ntn'),(l,ll)
 
+type local_univs = { bound : Univ.Level.t Id.Map.t; unb_univs : bool }
+
 type intern_env = {
-  ids: Names.Id.Set.t;
+  ids: Id.Set.t;
   unb: bool;
+  local_univs: local_univs;
   tmp_scope: Notation_term.tmp_scope_name option;
   scopes: Notation_term.scope_name list;
   impls: internalization_env;
@@ -1160,6 +1163,32 @@ let glob_sort_of_level (level: glob_level) : glob_sort =
   | UAnonymous {rigid} -> UAnonymous {rigid}
   | UNamed id -> UNamed [id,0]
 
+let intern_sort_name ~local_univs = function
+  | CSProp -> GSProp
+  | CProp -> GProp
+  | CSet -> GSet
+  | CRawType u -> GRawUniv u
+  | CType qid ->
+    let is_id = qualid_is_ident qid in
+    let local = if not is_id then None
+      else Id.Map.find_opt (qualid_basename qid) local_univs.bound
+    in
+    match local with
+    | Some u -> GUniv u
+    | None ->
+      try GUniv (Univ.Level.make (Nametab.locate_universe qid))
+      with Not_found ->
+        if is_id && local_univs.unb_univs
+        then GLocalUniv (CAst.make ?loc:qid.loc (qualid_basename qid))
+        else
+          CErrors.user_err Pp.(str "Undeclared universe " ++ pr_qualid qid ++ str".")
+
+let intern_sort ~local_univs s =
+  map_glob_sort_gen (List.map (on_fst (intern_sort_name ~local_univs))) s
+
+let intern_instance ~local_univs us =
+  Option.map (List.map (map_glob_sort_gen (intern_sort_name ~local_univs))) us
+
 (* Is it a global reference or a syntactic definition? *)
 let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
   let loc = qid.loc in
@@ -1225,6 +1254,7 @@ let check_applied_projection isproj realref qid =
 
 let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us args qid =
   let loc = qid.CAst.loc in
+  let us = intern_instance ~local_univs:env.local_univs us in
   if qualid_is_ident qid then
       try
         let res = intern_var env lvar namedctx loc (qualid_basename qid) us in
@@ -1256,7 +1286,8 @@ let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us
 let interp_reference vars r =
   let (r,_,_),_ =
     intern_applied_reference ~isproj:None (fun _ -> error_not_enough_arguments ?loc:None)
-      {ids = Id.Set.empty; unb = false ;
+      {ids = Id.Set.empty; unb = false;
+       local_univs = { bound=Id.Map.empty; unb_univs = false };(* <- doesn't matter here *)
        tmp_scope = None; scopes = []; impls = empty_internalization_env;
        binder_block_names = None}
       Environ.empty_named_context_val
@@ -2269,12 +2300,12 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
     (* end *)
     | CSort s ->
         DAst.make ?loc @@
-        GSort s
+        GSort (intern_sort ~local_univs:env.local_univs s)
     | CCast (c1, c2) ->
         DAst.make ?loc @@
         GCast (intern env c1, map_cast_type (intern_type (slide_binders env)) c2)
     | CArray(u,t,def,ty) ->
-      DAst.make ?loc @@ GArray(u, Array.map (intern env) t, intern env def, intern env ty)
+      DAst.make ?loc @@ GArray(intern_instance ~local_univs:env.local_univs u, Array.map (intern env) t, intern env def, intern env ty)
     )
   and intern_type env = intern (set_type_scope env)
 
@@ -2446,6 +2477,8 @@ let extract_ids env =
     (Termops.ids_of_rel_context (Environ.rel_context env))
     Id.Set.empty
 
+let bound_univs sigma = Evd.universe_binders sigma
+
 let scope_of_type_kind env sigma = function
   | IsType -> Notation.current_type_scope_name ()
   | OfType typ -> compute_type_scope env sigma typ
@@ -2468,8 +2501,9 @@ let intern_gen kind env sigma
   let tmp_scope = scope_of_type_kind env sigma kind in
   let k = allowed_binder_kind_of_type_kind kind in
   internalize env {ids = extract_ids env; unb = false;
-                         tmp_scope = tmp_scope; scopes = [];
-                         impls; binder_block_names = Some (k,Id.Map.domain impls)}
+                   local_univs = { bound = bound_univs sigma; unb_univs = true };
+                   tmp_scope = tmp_scope; scopes = [];
+                   impls; binder_block_names = Some (k,Id.Map.domain impls)}
     pattern_mode (ltacvars, Id.Map.empty) c
 
 let intern_constr env sigma c = intern_gen WithoutTypeConstraint env sigma c
@@ -2558,7 +2592,9 @@ let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
   let impls = empty_internalization_env in
   let k = allowed_binder_kind_of_type_kind kind in
   internalize env
-    {ids; unb = false; tmp_scope; scopes = []; impls;
+    {ids; unb = false;
+     local_univs = { bound = bound_univs sigma; unb_univs = true };
+     tmp_scope; scopes = []; impls;
      binder_block_names = Some (k,Id.Set.empty)}
     pattern_mode (ltacvars, vl) c
 
@@ -2568,8 +2604,11 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a =
   let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in
   let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in
   let c = internalize env
-    {ids; unb = false; tmp_scope = None; scopes = []; impls; binder_block_names = None}
-    false (empty_ltac_sign, vl) a in
+      {ids; unb = false;
+       local_univs = { bound = Id.Map.empty; unb_univs = false };
+       tmp_scope = None; scopes = []; impls; binder_block_names = None}
+      false (empty_ltac_sign, vl) a
+  in
   (* Splits variables into those that are binding, bound, or both *)
   (* Translate and check that [c] has all its free variables bound in [vars] *)
   let a, reversible = notation_constr_of_glob_constr nenv c in
@@ -2596,7 +2635,7 @@ let interp_binder_evars env sigma na t =
 let my_intern_constr env lvar acc c =
   internalize env acc false lvar c
 
-let intern_context env impl_env binders =
+let intern_context env ~bound_univs impl_env binders =
   let lvar = (empty_ltac_sign, Id.Map.empty) in
   let ids =
     (* We assume all ids around are parts of the prefix of the current
@@ -2607,6 +2646,7 @@ let intern_context env impl_env binders =
                let (env, bl) = intern_local_binder_aux (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in
                (env, bl))
             ({ids; unb = false;
+              local_univs = { bound = bound_univs; unb_univs = true };
               tmp_scope = None; scopes = []; impls = impl_env;
               binder_block_names = Some (Some AbsPi,ids)}, []) binders in
   (lenv.impls, List.map glob_local_binder_of_extended bl)
@@ -2643,17 +2683,21 @@ let interp_glob_context_evars ?(program_mode=false) env sigma bl =
   sigma, ((env, par), List.rev impls)
 
 let interp_context_evars ?program_mode ?(impl_env=empty_internalization_env) env sigma params =
-  let int_env,bl = intern_context env impl_env params in
+  let int_env,bl = intern_context env ~bound_univs:(bound_univs sigma) impl_env params in
   let sigma, x = interp_glob_context_evars ?program_mode env sigma bl in
   sigma, (int_env, x)
 
 
 (** Local universe and constraint declarations. *)
 
+let interp_known_level evd u =
+  let u = intern_sort_name ~local_univs:{bound = bound_univs evd; unb_univs=false} u in
+  Pretyping.known_glob_level evd u
+
 let interp_univ_constraints env evd cstrs =
   let interp (evd,cstrs) (u, d, u') =
-    let ul = Pretyping.interp_known_glob_level evd u in
-    let u'l = Pretyping.interp_known_glob_level evd u' in
+    let ul = interp_known_level evd u in
+    let u'l = interp_known_level evd u' in
     let cstr = (ul,d,u'l) in
     let cstrs' = Univ.Constraint.add cstr cstrs in
     try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 0de6c3e89d..f92a54e23f 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -88,7 +88,8 @@ val intern_gen : typing_constraint -> env -> evar_map ->
 val intern_pattern : env -> cases_pattern_expr ->
   lident list * (Id.t Id.Map.t * cases_pattern) list
 
-val intern_context : env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list
+val intern_context : env -> bound_univs:UnivNames.universe_binders ->
+  internalization_env -> local_binder_expr list -> internalization_env * glob_decl list
 
 (** {6 Composing internalization with type inference (pretyping) } *)
 
@@ -198,6 +199,8 @@ val check_duplicate : ?loc:Loc.t -> (qualid * constr_expr) list -> unit
 (** Check that a list of record field definitions doesn't contain
     duplicates. *)
 
+val interp_known_level : Evd.evar_map -> sort_name_expr -> Univ.Level.t
+
 (** Local universe and constraint declarations. *)
 val interp_univ_decl : Environ.env -> universe_decl_expr ->
                        Evd.evar_map * UState.universe_decl
diff --git a/kernel/names.ml b/kernel/names.ml
index 13761ca245..be65faf234 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -1115,3 +1115,5 @@ let eq_egr e1 e2 = match e1, e2 with
 type lident = Id.t CAst.t
 type lname = Name.t CAst.t
 type lstring = string CAst.t
+
+let lident_eq = CAst.eq Id.equal
diff --git a/kernel/names.mli b/kernel/names.mli
index 74a4e6f7d0..747299bb12 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -727,3 +727,5 @@ val eq_egr : evaluable_global_reference ->  evaluable_global_reference -> bool
 type lident = Id.t CAst.t
 type lname = Name.t CAst.t
 type lstring = string CAst.t
+
+val lident_eq : lident -> lident -> bool
diff --git a/lib/cAst.ml b/lib/cAst.ml
index 18fa1c9b0d..30b7fca587 100644
--- a/lib/cAst.ml
+++ b/lib/cAst.ml
@@ -24,3 +24,5 @@ let map_from_loc f l =
 
 let with_val f n = f n.v
 let with_loc_val f n = f ?loc:n.loc n.v
+
+let eq f x y = f x.v y.v
diff --git a/lib/cAst.mli b/lib/cAst.mli
index 2e07d1cd78..025bdf25ab 100644
--- a/lib/cAst.mli
+++ b/lib/cAst.mli
@@ -22,3 +22,5 @@ val map_from_loc : (?loc:Loc.t -> 'a -> 'b) -> 'a Loc.located -> 'b t
 
 val with_val : ('a -> 'b) -> 'a t -> 'b
 val with_loc_val : (?loc:Loc.t -> 'a -> 'b) -> 'a t -> 'b
+
+val eq : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
diff --git a/library/libnames.ml b/library/libnames.ml
index 88b2e41855..ba1ef1e2f9 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -145,6 +145,8 @@ let qualid_of_dirpath ?loc dir =
   let (l,a) = split_dirpath dir in
   make_qualid ?loc l a
 
+let qualid_of_lident lid = qualid_of_ident ?loc:lid.CAst.loc lid.CAst.v
+
 let qualid_is_ident qid =
   DirPath.is_empty qid.CAst.v.dirpath
 
diff --git a/library/libnames.mli b/library/libnames.mli
index a384510879..65aca0c87d 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -77,6 +77,7 @@ val qualid_of_string : ?loc:Loc.t -> string -> qualid
 val qualid_of_path : ?loc:Loc.t -> full_path -> qualid
 val qualid_of_dirpath : ?loc:Loc.t -> DirPath.t -> qualid
 val qualid_of_ident : ?loc:Loc.t -> Id.t -> qualid
+val qualid_of_lident : lident -> qualid
 
 val qualid_is_ident : qualid -> bool
 val qualid_path : qualid -> DirPath.t
diff --git a/library/nametab.ml b/library/nametab.ml
index a51c281f2b..d5cc4f8ac5 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -562,9 +562,9 @@ let shortest_qualid_of_modtype ?loc kn =
   let sp = MPmap.find kn !the_modtyperevtab in
     MPTab.shortest_qualid ?loc Id.Set.empty sp !the_modtypetab
 
-let shortest_qualid_of_universe ?loc kn =
+let shortest_qualid_of_universe ?loc ctx kn =
   let sp = UnivIdMap.find kn !the_univrevtab in
-    UnivTab.shortest_qualid ?loc Id.Set.empty sp !the_univtab
+    UnivTab.shortest_qualid ?loc ctx sp !the_univtab
 
 let pr_global_env env ref =
   try pr_qualid (shortest_qualid_of_global env ref)
diff --git a/library/nametab.mli b/library/nametab.mli
index 8a8b59733c..fa27dcab9a 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -206,7 +206,7 @@ val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
 val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid
 val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid
 val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid
-val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.UGlobal.t -> qualid
+val shortest_qualid_of_universe : ?loc:Loc.t -> Id.Set.t -> Univ.Level.UGlobal.t -> qualid
 
 (** {5 Generic name handling} *)
 
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 68530178f8..efe4bfd7f6 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -106,9 +106,9 @@ GRAMMAR EXTEND Gram
     [ [ c = lconstr -> { c } ] ]
   ;
   sort:
-    [ [ "Set"  -> { UNamed [GSet,0] }
-      | "Prop" -> { UNamed [GProp,0] }
-      | "SProp" -> { UNamed [GSProp,0] }
+    [ [ "Set"  -> { UNamed [CSet,0] }
+      | "Prop" -> { UNamed [CProp,0] }
+      | "SProp" -> { UNamed [CSProp,0] }
       | "Type" -> { UAnonymous {rigid=true} }
       | "Type"; "@{"; "_"; "}" -> { UAnonymous {rigid=false} }
       | "Type"; "@{"; u = universe; "}" -> { UNamed u } ] ]
@@ -124,9 +124,9 @@ GRAMMAR EXTEND Gram
       | -> { 0 } ] ]
   ;
   universe_name:
-    [ [ id = global -> { GType id }
-      | "Set"  -> { GSet }
-      | "Prop" -> { GProp } ] ]
+    [ [ id = global -> { CType id }
+      | "Set"  -> { CSet }
+      | "Prop" -> { CProp } ] ]
   ;
   universe_expr:
     [ [ id = universe_name; n = universe_increment -> { (id,n) } ] ]
@@ -282,12 +282,12 @@ GRAMMAR EXTEND Gram
       | -> { None } ] ]
   ;
   universe_level:
-    [ [ "Set" -> { UNamed GSet }
+    [ [ "Set" -> { UNamed CSet }
       (* no parsing SProp as a level *)
-      | "Prop" -> { UNamed GProp }
+      | "Prop" -> { UNamed CProp }
       | "Type" -> { UAnonymous {rigid=true} }
       | "_" -> { UAnonymous {rigid=false} }
-      | id = global -> { UNamed (GType id) } ] ]
+      | id = global -> { UNamed (CType id) } ] ]
   ;
   fix_decls:
     [ [ dcl = fix_decl -> { let (id,_,_,_,_) = dcl.CAst.v in (id,[dcl.CAst.v]) }
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index df9084ab76..8bff5cfd94 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -187,9 +187,9 @@ module Constr :
       [@@deprecated "Deprecated in 8.13; use 'term' instead"]
     val ident : Id.t Entry.t
     val global : qualid Entry.t
-    val universe_name : Glob_term.glob_sort_name Entry.t
-    val universe_level : Glob_term.glob_level Entry.t
-    val sort : Glob_term.glob_sort Entry.t
+    val universe_name : sort_name_expr Entry.t
+    val universe_level : univ_level_expr Entry.t
+    val sort : sort_expr Entry.t
     val sort_family : Sorts.family Entry.t
     val pattern : cases_pattern_expr Entry.t
     val constr_pattern : constr_expr Entry.t
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index c485c38009..23a7b89d2c 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -443,7 +443,7 @@ let cc_tactic depth additionnal_terms =
       let pr_missing (c, missing) =
         let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in
         let holes = List.init missing (fun _ -> hole) in
-        Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes))
+        Printer.pr_glob_constr_env env sigma (DAst.make @@ GApp (c, holes))
       in
             let msg = Pp.(str "Goal is solvable by congruence but some arguments are missing."
                     ++ fnl () ++
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 767a9ec39b..5bfb37f4cb 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -458,9 +458,11 @@ let rec pattern_to_term_and_type env typ =
    but only the value of the function
 *)
 
+let pr_glob_constr_env env x = pr_glob_constr_env env (Evd.from_env env) x
+
 let rec build_entry_lc env sigma funnames avoid rt :
     glob_constr build_entry_return =
-  observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt);
+  observe (str " Entering : " ++ pr_glob_constr_env env rt);
   let open CAst in
   match DAst.get rt with
   | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _
@@ -638,9 +640,7 @@ let rec build_entry_lc env sigma funnames avoid rt :
       with Not_found ->
         user_err
           ( str "Cannot find the inductive associated to "
-          ++ Printer.pr_glob_constr_env env b
-          ++ str " in "
-          ++ Printer.pr_glob_constr_env env rt
+          ++ pr_glob_constr_env env b ++ str " in " ++ pr_glob_constr_env env rt
           ++ str ". try again with a cast" )
     in
     let case_pats = build_constructors_of_type (fst ind) [] in
@@ -662,9 +662,7 @@ let rec build_entry_lc env sigma funnames avoid rt :
       with Not_found ->
         user_err
           ( str "Cannot find the inductive associated to "
-          ++ Printer.pr_glob_constr_env env b
-          ++ str " in "
-          ++ Printer.pr_glob_constr_env env rt
+          ++ pr_glob_constr_env env b ++ str " in " ++ pr_glob_constr_env env rt
           ++ str ". try again with a cast" )
     in
     let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in
@@ -1321,11 +1319,11 @@ let do_build_inductive evd (funconstants : pconstant list)
             @@ Constrexpr.CLetIn
                  ( CAst.make n
                  , with_full_print
-                     (Constrextern.extern_glob_constr Id.Set.empty)
+                     Constrextern.(extern_glob_constr empty_extern_env)
                      t
                  , Some
                      (with_full_print
-                        (Constrextern.extern_glob_constr Id.Set.empty)
+                        Constrextern.(extern_glob_constr empty_extern_env)
                         typ)
                  , acc )
           | None ->
@@ -1335,7 +1333,7 @@ let do_build_inductive evd (funconstants : pconstant list)
                        ( [CAst.make n]
                        , Constrexpr_ops.default_binder_kind
                        , with_full_print
-                           (Constrextern.extern_glob_constr Id.Set.empty)
+                           Constrextern.(extern_glob_constr empty_extern_env)
                            t ) ]
                  , acc ))
         rel_first_args
@@ -1410,11 +1408,11 @@ let do_build_inductive evd (funconstants : pconstant list)
           @@ Constrexpr.CLetIn
                ( CAst.make n
                , with_full_print
-                   (Constrextern.extern_glob_constr Id.Set.empty)
+                   Constrextern.(extern_glob_constr empty_extern_env)
                    t
                , Some
                    (with_full_print
-                      (Constrextern.extern_glob_constr Id.Set.empty)
+                      Constrextern.(extern_glob_constr empty_extern_env)
                       typ)
                , acc )
         | None ->
@@ -1424,7 +1422,7 @@ let do_build_inductive evd (funconstants : pconstant list)
                      ( [CAst.make n]
                      , Constrexpr_ops.default_binder_kind
                      , with_full_print
-                         (Constrextern.extern_glob_constr Id.Set.empty)
+                         Constrextern.(extern_glob_constr empty_extern_env)
                          t ) ]
                , acc ))
       rel_first_args
@@ -1448,16 +1446,16 @@ let do_build_inductive evd (funconstants : pconstant list)
         | Some typ ->
           Constrexpr.CLocalDef
             ( CAst.make n
-            , Constrextern.extern_glob_constr Id.Set.empty t
+            , Constrextern.(extern_glob_constr empty_extern_env) t
             , Some
                 (with_full_print
-                   (Constrextern.extern_glob_constr Id.Set.empty)
+                   Constrextern.(extern_glob_constr empty_extern_env)
                    typ) )
         | None ->
           Constrexpr.CLocalAssum
             ( [CAst.make n]
             , Constrexpr_ops.default_binder_kind
-            , Constrextern.extern_glob_constr Id.Set.empty t ))
+            , Constrextern.(extern_glob_constr empty_extern_env) t ))
       rels_params
   in
   let ext_rels_constructors =
@@ -1466,7 +1464,7 @@ let do_build_inductive evd (funconstants : pconstant list)
            ( false
            , ( CAst.make id
              , with_full_print
-                 (Constrextern.extern_glob_type Id.Set.empty)
+                 Constrextern.(extern_glob_type empty_extern_env)
                  ((* zeta_normalize *) alpha_rt rel_params_ids t) ) )))
       rel_constructors
   in
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index ff4a82f864..daed855600 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -150,7 +150,7 @@ let pr_occurrences = pr_occurrences () () ()
 let pr_gen env sigma prc _prlc _prtac x = prc env sigma x
 
 let pr_globc env sigma _prc _prlc _prtac (_,glob) =
-  Printer.pr_glob_constr_env env glob
+  Printer.pr_glob_constr_env env sigma glob
 
 let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t)
 
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index eed9419946..069a342b2a 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -63,7 +63,7 @@ let eval_uconstrs ist cs =
 
 let pr_auto_using_raw env sigma _ _ _  = Pptactic.pr_auto_using @@ Ppconstr.pr_constr_expr env sigma
 let pr_auto_using_glob env sigma _ _ _ = Pptactic.pr_auto_using (fun (c,_) ->
-    Printer.pr_glob_constr_env env c)
+    Printer.pr_glob_constr_env env sigma c)
 let pr_auto_using env sigma _ _ _ = Pptactic.pr_auto_using @@
      Printer.pr_closed_glob_env env sigma
 
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index a3f03b5bb5..f12ca0685e 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -40,9 +40,9 @@ type glob_constr_with_bindings = glob_constr_and_expr with_bindings
 type glob_constr_with_bindings_sign = interp_sign * glob_constr_and_expr with_bindings
 
 let pr_glob_constr_with_bindings_sign env sigma _ _ _ (ge : glob_constr_with_bindings_sign) =
-  Printer.pr_glob_constr_env env (fst (fst (snd ge)))
+  Printer.pr_glob_constr_env env sigma (fst (fst (snd ge)))
 let pr_glob_constr_with_bindings env sigma _ _ _ (ge : glob_constr_with_bindings) =
-  Printer.pr_glob_constr_env env (fst (fst ge))
+  Printer.pr_glob_constr_env env sigma (fst (fst ge))
 let pr_constr_expr_with_bindings env sigma prc _ _ (ge : constr_expr_with_bindings) = prc env sigma (fst ge)
 let interp_glob_constr_with_bindings ist gl c = Tacmach.project gl , (ist, c)
 let glob_glob_constr_with_bindings ist l = Tacintern.intern_constr_with_bindings ist l
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index cd7b1f7f28..fa5bbf7676 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1130,12 +1130,12 @@ let pr_goal_selector ~toplevel s =
     let rec prtac n (t:glob_tactic_expr) =
       let pr = {
         pr_tactic = prtac;
-        pr_constr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env));
-        pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env));
-        pr_lconstr = (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env));
-        pr_pattern = (fun env sigma -> pr_pat_and_constr_expr (pr_glob_constr_env env));
+        pr_constr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma));
+        pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma));
+        pr_lconstr = (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env sigma));
+        pr_pattern = (fun env sigma -> pr_pat_and_constr_expr (pr_glob_constr_env env sigma));
         pr_constant = pr_or_var (pr_and_short_name (pr_evaluable_reference_env env));
-        pr_lpattern = (fun env sigma -> pr_pat_and_constr_expr (pr_lglob_constr_env env));
+        pr_lpattern = (fun env sigma -> pr_pat_and_constr_expr (pr_lglob_constr_env env sigma));
         pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant);
         pr_name = pr_lident;
         pr_generic = Pputils.pr_glb_generic;
@@ -1166,7 +1166,7 @@ let pr_goal_selector ~toplevel s =
       let pr = {
         pr_tactic = (fun _ _ -> str "<tactic>");
         pr_constr = pr_econstr_env;
-        pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env));
+        pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma));
         pr_lconstr = pr_leconstr_env;
         pr_pattern = pr_constr_pattern_env;
         pr_lpattern = pr_lconstr_pattern_env;
@@ -1189,7 +1189,7 @@ let pr_goal_selector ~toplevel s =
 
   let pr_raw_extend env sigma = pr_raw_extend_rec @@ pr_raw_tactic_level env sigma
 
-  let pr_glob_extend env sigma = pr_glob_extend_rec (pr_glob_tactic_level env)
+  let pr_glob_extend env = pr_glob_extend_rec (pr_glob_tactic_level env)
 
   let pr_alias pr lev key args =
     pr_alias_gen (fun _ arg -> pr arg) lev key args
@@ -1212,8 +1212,8 @@ let declare_extra_genarg_pprule wit
         f env sigma pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in
   let g x =
     Genprint.PrinterBasic (fun env sigma ->
-    g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env))
-      (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env))
+    g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma))
+      (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env sigma))
       (fun env sigma -> pr_glob_tactic_level env) x)
   in
   let h x =
@@ -1242,8 +1242,8 @@ let declare_extra_genarg_pprule_with_level wit
         default_already_surrounded = default_surrounded;
         default_ensure_surrounded = default_non_surrounded;
         printer = (fun env sigma n ->
-          g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env))
-            (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env))
+          g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma))
+            (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env sigma))
             (fun env sigma -> pr_glob_tactic_level env) n x) }
   in
   let h x =
@@ -1301,10 +1301,10 @@ let register_basic_print0 wit f g h =
   Genprint.register_print0 wit (lift f) (lift g) (lift_top h)
 
 let pr_glob_constr_pptac env sigma c =
-  pr_glob_constr_env env c
+  pr_glob_constr_env env sigma c
 
 let pr_lglob_constr_pptac env sigma c =
-  pr_lglob_constr_env env c
+  pr_lglob_constr_env env sigma c
 
 let pr_raw_intro_pattern =
   lift_env (fun env sigma -> Miscprint.pr_intro_pattern @@ pr_constr_expr env sigma)
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 5e199dad62..79e0adf9f7 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -124,7 +124,7 @@ val pr_glb_generic : env -> Evd.evar_map -> glevel generic_argument -> Pp.t
 val pr_raw_extend: env -> Evd.evar_map -> int ->
   ml_tactic_entry -> raw_tactic_arg list -> Pp.t
 
-val pr_glob_extend: env -> Evd.evar_map -> int ->
+val pr_glob_extend: env -> int ->
   ml_tactic_entry -> glob_tactic_arg list -> Pp.t
 
 val pr_extend :
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 9c15d24dd3..aa2449d962 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -244,7 +244,8 @@ let string_of_call ck =
          (Pptactic.pr_glob_tactic (Global.env ())
             (Tacexpr.TacAtom (CAst.make te)))
        | Tacexpr.LtacConstrInterp (c, _) ->
-         pr_glob_constr_env (Global.env ()) c
+         let env = Global.env () in
+         pr_glob_constr_env env (Evd.from_env env) c
        | Tacexpr.LtacMLCall te ->
          (Pptactic.pr_glob_tactic (Global.env ())
             te)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 00ac155f0e..f2241e78d2 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -773,7 +773,7 @@ let interp_may_eval f ist env sigma = function
           function already use effect, I call [run] hoping it doesn't mess
           up with any assumption. *)
        Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () ->
-         str"interpretation of term " ++ pr_glob_constr_env env (fst c)));
+         str"interpretation of term " ++ pr_glob_constr_env env sigma (fst c)));
        Exninfo.iraise reraise
 
 (* Interprets a constr expression possibly to first evaluate *)
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 5fbea4eeef..c4c528d373 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -16,11 +16,12 @@ open Tacexpr
 let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make ()
 
 let prtac x =
-  Pptactic.pr_glob_tactic (Global.env()) x
+  let env = Global.env () in
+  Pptactic.pr_glob_tactic env x
 let prmatchpatt env sigma hyp =
   Pptactic.pr_match_pattern (Printer.pr_constr_pattern_env env sigma) hyp
 let prmatchrl env sigma rl =
-  Pptactic.pr_match_rule false (Pptactic.pr_glob_tactic (Global.env()))
+  Pptactic.pr_match_rule false prtac
     (fun (_,p) -> Printer.pr_constr_pattern_env env sigma p) rl
 
 (* This module intends to be a beginning of debugger for tactic expressions.
@@ -366,24 +367,22 @@ let explain_ltac_call_trace last trace loc =
     | Tacexpr.LtacNotationCall kn -> quote (Pptactic.pr_alias_key kn)
   | Tacexpr.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst)
   | Tacexpr.LtacMLCall t ->
-      quote (Pptactic.pr_glob_tactic (Global.env()) t)
+      quote (prtac t)
   | Tacexpr.LtacVarCall (id,t) ->
       quote (Id.print id) ++ strbrk " (bound to " ++
-        Pptactic.pr_glob_tactic (Global.env()) t ++ str ")"
+        prtac t ++ str ")"
   | Tacexpr.LtacAtomCall te ->
-      quote (Pptactic.pr_glob_tactic (Global.env())
-              (Tacexpr.TacAtom (CAst.make te)))
+      quote (prtac (Tacexpr.TacAtom (CAst.make te)))
   | Tacexpr.LtacConstrInterp (c, { Ltac_pretype.ltac_constrs = vars }) ->
-      quote (Printer.pr_glob_constr_env (Global.env()) c) ++
+    (* XXX: This hooks into the CErrors's additional error info API so
+       it is tricky to provide the right env for now. *)
+      let env = Global.env() in
+      let sigma = Evd.from_env env in
+      quote (Printer.pr_glob_constr_env env sigma c) ++
         (if not (Id.Map.is_empty vars) then
           strbrk " (with " ++
             prlist_with_sep pr_comma
             (fun (id,c) ->
-              (* XXX: This hooks into the CErrors's additional error
-                 info API so it is tricky to provide the right env for
-                 now. *)
-              let env = Global.env () in
-              let sigma = Evd.from_env env in
               Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders_env env sigma c)
             (List.rev (Id.Map.bindings vars)) ++ str ")"
         else mt())
diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index 42b9248979..61643c2aa3 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -50,7 +50,7 @@ let interp_agen ist gl ((goclr, _), (k, gc as c)) (clr, rcs) =
         SsrHyp (Loc.tag ?loc id) :: clr', rcs'
     | _ -> clr', rcs'
 
-let pf_pr_glob_constr gl = pr_glob_constr_env (pf_env gl)
+let pf_pr_glob_constr gl = pr_glob_constr_env (pf_env gl) (project gl)
 
 let interp_nbargs ist gl rc =
   try
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index cb58b9bcb8..cd219838d5 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -895,7 +895,7 @@ open Constrexpr
 open Util
 
 (** Constructors for constr_expr *)
-let mkCProp loc = CAst.make ?loc @@ CSort (UNamed [GProp,0])
+let mkCProp loc = CAst.make ?loc @@ CSort (UNamed [CProp,0])
 let mkCType loc = CAst.make ?loc @@ CSort (UAnonymous {rigid=true})
 let mkCVar ?loc id = CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None)
 let rec mkCHoles ?loc n =
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index a7ebd5f9f5..fdfba48024 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -84,7 +84,7 @@ let interp_congrarg_at ist gl n rf ty m =
     if i + n > m then None else
     try
       let rt = mkRApp congrn (args1 @  mkRApp rf (mkRHoles i) :: args2) in
-      ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) rt));
+      ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) (project gl) rt));
       Some (interp_refine ist gl rt)
     with _ -> loop (i + 1) in
   loop 0
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index ab36d4fc7c..95c8024e89 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -57,17 +57,16 @@ let pr_guarded guard prc c =
   let s = Format.flush_str_formatter () ^ "$" in
   if guard s (skip_wschars s 0) then pr_paren prc c else prc c
 
-let prl_constr_expr =
+let with_global_env_evm f x =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  Ppconstr.pr_lconstr_expr env sigma
-let pr_glob_constr c = Printer.pr_glob_constr_env (Global.env ()) c
-let prl_glob_constr c = Printer.pr_lglob_constr_env (Global.env ()) c
+  f env sigma x
+
+let prl_constr_expr = with_global_env_evm Ppconstr.pr_lconstr_expr
+let pr_glob_constr = with_global_env_evm Printer.pr_glob_constr_env
+let prl_glob_constr = with_global_env_evm Printer.pr_lglob_constr_env
 let pr_glob_constr_and_expr = function
-  | _, Some c ->
-    let env = Global.env () in
-    let sigma = Evd.from_env env in
-    Ppconstr.pr_constr_expr env sigma c
+  | _, Some c -> with_global_env_evm Ppconstr.pr_constr_expr c
   | c, None -> pr_glob_constr c
 let pr_term (k, c) = pr_guarded (guard_term k) pr_glob_constr_and_expr c
 
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 99cf197b78..3e44bd4d3b 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -203,8 +203,8 @@ let pr_raw_ssrhintref env sigma prc _ _ = let open CAst in function
 let pr_rawhintref env sigma c =
   match DAst.get c with
   | GApp (f, args) when isRHoles args ->
-    pr_glob_constr_env env f ++ str "|" ++ int (List.length args)
-  | _ -> pr_glob_constr_env env c
+    pr_glob_constr_env env sigma f ++ str "|" ++ int (List.length args)
+  | _ -> pr_glob_constr_env env sigma c
 
 let pr_glob_ssrhintref env sigma _ _ _ (c, _) = pr_rawhintref env sigma c
 
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index d99ead139d..97926753f5 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -195,7 +195,7 @@ let interp_glob ist glob = Goal.enter_one ~__LOC__ begin fun goal ->
   let env = Goal.env goal in
   let sigma = Goal.sigma goal in
   Ssrprinters.ppdebug (lazy
-    Pp.(str"interp-in: " ++ Printer.pr_glob_constr_env env glob));
+    Pp.(str"interp-in: " ++ Printer.pr_glob_constr_env env sigma glob));
   try
     let sigma,term = Tacinterp.interp_open_constr ist env sigma (glob,None) in
     Ssrprinters.ppdebug (lazy
@@ -205,7 +205,7 @@ let interp_glob ist glob = Goal.enter_one ~__LOC__ begin fun goal ->
     (* XXX this is another catch all! *)
     let e, info = Exninfo.capture e in
     Ssrprinters.ppdebug (lazy
-    Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env glob));
+    Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env sigma glob));
     tclZERO ~info e
 end
 
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index a4aa08300d..ea014250ca 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -88,8 +88,12 @@ let pr_guarded guard prc c =
   let s = Pp.string_of_ppcmds (prc c) ^ "$" in
   if guard s (skip_wschars s 0) then pr_paren prc c else prc c
 (* More sensible names for constr printers *)
-let prl_glob_constr c = pr_lglob_constr_env (Global.env ()) c
-let pr_glob_constr c = pr_glob_constr_env (Global.env ()) c
+let with_global_env_evm f x =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  f env sigma x
+let prl_glob_constr = with_global_env_evm pr_lglob_constr_env
+let pr_glob_constr = with_global_env_evm pr_glob_constr_env
 let prl_constr_expr = pr_lconstr_expr
 let pr_constr_expr = pr_constr_expr
 let prl_glob_constr_and_expr env sigma = function
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index a12a832f76..402a6f6ed3 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -648,26 +648,16 @@ let detype_cofix detype flags avoid env sigma n (names,tys,bodies) =
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
 
-(* TODO use some algebraic type with a case for unnamed univs so we
-   can cleanly detype them. NB: this corresponds to a hack in
-   Pretyping.interp_universe_level_name to convert Foo.xx strings into
-   universes. *)
-let hack_qualid_of_univ_level sigma l =
-  match Termops.reference_of_level sigma l with
-  | Some qid -> qid
-  | None ->
-    let path = String.split_on_char '.' (Univ.Level.to_string l) in
-    let path = List.rev_map Id.of_string_soft path in
-    Libnames.qualid_of_dirpath (DirPath.make path)
+let detype_level_name sigma l =
+  if Univ.Level.is_sprop l then GSProp else
+  if Univ.Level.is_prop l then GProp else
+  if Univ.Level.is_set l then GSet else
+    match UState.id_of_level (Evd.evar_universe_context sigma) l with
+    | Some id -> GLocalUniv (CAst.make id)
+    | None -> GUniv l
 
 let detype_universe sigma u =
-  let fn (l, n) =
-    let s =
-      if Univ.Level.is_prop l then GProp else
-      if Univ.Level.is_set l then GSet else
-      GType (hack_qualid_of_univ_level sigma l) in
-    (s, n) in
-  List.map fn (Univ.Universe.repr u)
+  List.map (on_fst (detype_level_name sigma)) (Univ.Universe.repr u)
 
 let detype_sort sigma = function
   | SProp -> UNamed [GSProp,0]
@@ -684,8 +674,7 @@ type binder_kind = BProd | BLambda | BLetIn
 (* Main detyping function                                             *)
 
 let detype_level sigma l =
-  let l = hack_qualid_of_univ_level sigma l in
-  UNamed (GType l)
+  UNamed (detype_level_name sigma l)
 
 let detype_instance sigma l =
   let l = EInstance.kind sigma l in
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index f42c754ef5..86d2cc78e0 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -48,8 +48,10 @@ let glob_sort_name_eq g1 g2 = match g1, g2 with
   | GSProp, GSProp
   | GProp, GProp
   | GSet, GSet -> true
-  | GType u1, GType u2 -> Libnames.qualid_eq u1 u2
-  | (GSProp|GProp|GSet|GType _), _ -> false
+  | GUniv u1, GUniv u2 -> Univ.Level.equal u1 u2
+  | GLocalUniv u1, GLocalUniv u2 -> lident_eq u1 u2
+  | GRawUniv u1, GRawUniv u2 -> Univ.Level.equal u1 u2
+  | (GSProp|GProp|GSet|GUniv _|GLocalUniv _|GRawUniv _), _ -> false
 
 exception ComplexSort
 
@@ -60,19 +62,23 @@ let glob_sort_family = let open Sorts in function
   | UNamed [GSet,0] -> InSet
   | _ -> raise ComplexSort
 
-let glob_sort_expr_eq f u1 u2 =
+let map_glob_sort_gen f = function
+  | UNamed l -> UNamed (f l)
+  | UAnonymous _ as x -> x
+
+let glob_sort_gen_eq f u1 u2 =
  match u1, u2 with
   | UAnonymous {rigid=r1}, UAnonymous {rigid=r2} -> r1 = r2
   | UNamed l1, UNamed l2 -> f l1 l2
   | (UNamed _ | UAnonymous _), _ -> false
 
 let glob_sort_eq u1 u2 =
-  glob_sort_expr_eq
+  glob_sort_gen_eq
     (List.equal (fun (x,m) (y,n) -> glob_sort_name_eq x y && Int.equal m n))
     u1 u2
 
 let glob_level_eq u1 u2 =
-  glob_sort_expr_eq glob_sort_name_eq u1 u2
+  glob_sort_gen_eq glob_sort_name_eq u1 u2
 
 let binding_kind_eq bk1 bk2 = match bk1, bk2 with
   | Explicit, Explicit -> true
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 6da8173dce..5ad1a207f3 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -11,8 +11,12 @@
 open Names
 open Glob_term
 
+val map_glob_sort_gen : ('a -> 'b) -> 'a glob_sort_gen -> 'b glob_sort_gen
+
 (** Equalities *)
 
+val glob_sort_gen_eq : ('a -> 'a -> bool) -> 'a glob_sort_gen -> 'a glob_sort_gen -> bool
+
 val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
 
 val glob_level_eq : Glob_term.glob_level -> Glob_term.glob_level -> bool
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index a49c8abe26..a957bc0fcd 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -26,17 +26,23 @@ type glob_sort_name =
   | GSProp (** representation of [SProp] literal *)
   | GProp (** representation of [Prop] level *)
   | GSet  (** representation of [Set] level *)
-  | GType of Libnames.qualid (** representation of a [Type] level *)
+  | GUniv of Univ.Level.t
+  | GLocalUniv of lident (** Locally bound universes (may also be nonstrict declaration) *)
+  | GRawUniv of Univ.Level.t
+  (** Hack for funind, DO NOT USE
 
-type 'a glob_sort_expr =
+      Note that producing the similar Constrexpr.CRawType for printing
+      is OK, just don't try to reinterp it. *)
+
+type 'a glob_sort_gen =
   | UAnonymous of { rigid : bool } (** not rigid = unifiable by minimization *)
   | UNamed of 'a
 
 (** levels, occurring in universe instances *)
-type glob_level = glob_sort_name glob_sort_expr
+type glob_level = glob_sort_name glob_sort_gen
 
 (** sort expressions *)
-type glob_sort = (glob_sort_name * int) list glob_sort_expr
+type glob_sort = (glob_sort_name * int) list glob_sort_gen
 
 type glob_constraint = glob_sort_name * Univ.constraint_type * glob_sort_name
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f52dfc51ac..9dbded75ba 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -130,53 +130,32 @@ let is_strict_universe_declarations =
 
 (** Miscellaneous interpretation functions *)
 
-let interp_known_universe_level_name evd qid =
-  try
-    let open Libnames in
-    if qualid_is_ident qid then Evd.universe_of_name evd @@ qualid_basename qid
-    else raise Not_found
+let universe_level_name evd ({CAst.v=id} as lid) =
+  try evd, Evd.universe_of_name evd id
   with Not_found ->
-    let qid = Nametab.locate_universe qid in
-    Univ.Level.make qid
+    if not (is_strict_universe_declarations ()) then
+      new_univ_level_variable ?loc:lid.CAst.loc ~name:id univ_rigid evd
+    else user_err ?loc:lid.CAst.loc ~hdr:"universe_level_name"
+        (Pp.(str "Undeclared universe: " ++ Id.print id))
 
-let interp_universe_level_name evd qid =
-  try evd, interp_known_universe_level_name evd qid
-  with Not_found ->
-    if Libnames.qualid_is_ident qid then (* Undeclared *)
-      let id = Libnames.qualid_basename qid in
-      if not (is_strict_universe_declarations ()) then
-        new_univ_level_variable ?loc:qid.CAst.loc ~name:id univ_rigid evd
-      else user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name"
-          (Pp.(str "Undeclared universe: " ++ Id.print id))
-    else
-      let dp, i = Libnames.repr_qualid qid in
-      let num =
-        try int_of_string (Id.to_string i)
-        with Failure _ ->
-          user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name"
-            (Pp.(str "Undeclared global universe: " ++ Libnames.pr_qualid qid))
-      in
-      let level = Univ.Level.(make (UGlobal.make dp num)) in
-      let evd =
-        try Evd.add_global_univ evd level
-        with UGraph.AlreadyDeclared -> evd
-      in evd, level
-
-let interp_sort_name sigma = function
+let sort_name sigma = function
   | GSProp -> sigma, Univ.Level.sprop
   | GProp -> sigma, Univ.Level.prop
   | GSet -> sigma, Univ.Level.set
-  | GType l -> interp_universe_level_name sigma l
+  | GUniv u -> sigma, u
+  | GRawUniv u ->
+    (try Evd.add_global_univ sigma u with UGraph.AlreadyDeclared -> sigma), u
+  | GLocalUniv l -> universe_level_name sigma l
 
-let interp_sort_info ?loc evd l =
+let sort_info ?loc evd l =
     List.fold_left (fun (evd, u) (l,n) ->
-      let evd', u' = interp_sort_name evd l in
+      let evd', u' = sort_name evd l in
       let u' = Univ.Universe.make u' in
       let u' = match n with
       | 0 -> u'
       | 1 -> Univ.Universe.super u'
       | n ->
-        user_err ?loc ~hdr:"interp_universe"
+        user_err ?loc ~hdr:"sort_info"
           (Pp.(str "Cannot interpret universe increment +" ++ int n))
       in (evd', Univ.sup u u'))
     (evd, Univ.Universe.type0m) l
@@ -393,24 +372,33 @@ let pretype_id pretype loc env sigma id =
 (*************************************************************************)
 (* Main pretyping function                                               *)
 
-let interp_known_glob_level ?loc evd = function
+let known_universe_level_name evd lid =
+  try Evd.universe_of_name evd lid.CAst.v
+  with Not_found ->
+    let u = Nametab.locate_universe (Libnames.qualid_of_lident lid) in
+    Univ.Level.make u
+
+let known_glob_level evd = function
   | GSProp -> Univ.Level.sprop
   | GProp -> Univ.Level.prop
   | GSet -> Univ.Level.set
-  | GType qid ->
-    try interp_known_universe_level_name evd qid
+  | GUniv u -> u
+  | GRawUniv u -> anomaly Pp.(str "Raw universe in known_glob_level.")
+  | GLocalUniv lid ->
+    try known_universe_level_name evd lid
     with Not_found ->
-      user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_qualid qid)
+      user_err ?loc:lid.CAst.loc ~hdr:"known_level_info"
+        (str "Undeclared universe " ++ Id.print lid.CAst.v)
 
-let interp_glob_level ?loc evd : glob_level -> _ = function
+let glob_level ?loc evd : glob_level -> _ = function
   | UAnonymous {rigid} -> new_univ_level_variable ?loc (if rigid then univ_rigid else univ_flexible) evd
-  | UNamed s -> interp_sort_name evd s
+  | UNamed s -> sort_name evd s
 
-let interp_instance ?loc evd l =
+let instance ?loc evd l =
   let evd, l' =
     List.fold_left
       (fun (evd, univs) l ->
-         let evd, l = interp_glob_level ?loc evd l in
+         let evd, l = glob_level ?loc evd l in
          (evd, l :: univs)) (evd, [])
       l
   in
@@ -424,7 +412,7 @@ let pretype_global ?loc rigid env evd gr us =
   let evd, instance =
     match us with
     | None -> evd, None
-    | Some l -> interp_instance ?loc evd l
+    | Some l -> instance ?loc evd l
   in
   Evd.fresh_global ?loc ~rigid ?names:instance !!env evd gr
 
@@ -451,11 +439,11 @@ let pretype_ref ?loc sigma env ref us =
     let sigma, ty = type_of !!env sigma c in
     sigma, make_judge c ty
 
-let interp_sort ?loc evd : glob_sort -> _ = function
+let sort ?loc evd : glob_sort -> _ = function
   | UAnonymous {rigid} ->
     let evd, l = new_univ_level_variable ?loc (if rigid then univ_rigid else univ_flexible) evd in
     evd, Univ.Universe.make l
-  | UNamed l -> interp_sort_info ?loc evd l
+  | UNamed l -> sort_info ?loc evd l
 
 let judge_of_sort ?loc evd s =
   let judge =
@@ -469,7 +457,7 @@ let pretype_sort ?loc sigma s =
   | UNamed [GProp,0] -> sigma, judge_of_prop
   | UNamed [GSet,0] -> sigma, judge_of_set
   | _ ->
-  let sigma, s = interp_sort ?loc sigma s in
+  let sigma, s = sort ?loc sigma s in
   judge_of_sort ?loc sigma s
 
 let new_typed_evar env sigma ?naming ~src tycon =
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 7bb4a6e273..5668098fe6 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -30,8 +30,7 @@ val get_bidirectionality_hint : GlobRef.t -> int option
 
 val clear_bidirectionality_hint : GlobRef.t -> unit
 
-val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map ->
-  glob_sort_name -> Univ.Level.t
+val known_glob_level : Evd.evar_map -> glob_sort_name -> Univ.Level.t
 
 (** An auxiliary function for searching for fixpoint guard indexes *)
 
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 8942bc7805..4c410c3170 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -152,14 +152,15 @@ let tag_var = tag Tag.variable
 
   let pr_sep_com sep f c = pr_with_comments ?loc:(constr_loc c) (sep() ++ f c)
 
-  let pr_glob_sort_name = function
-    | GSProp -> str "SProp"
-    | GProp -> str "Prop"
-    | GSet -> str "Set"
-    | GType qid -> pr_qualid qid
+  let pr_sort_name_expr = function
+    | CSProp -> str "SProp"
+    | CProp -> str "Prop"
+    | CSet -> str "Set"
+    | CType qid -> pr_qualid qid
+    | CRawType s -> Univ.Level.pr s
 
   let pr_univ_expr (u,n) =
-    pr_glob_sort_name u ++ (match n with 0 -> mt () | _ -> str"+" ++ int n)
+    pr_sort_name_expr u ++ (match n with 0 -> mt () | _ -> str"+" ++ int n)
 
   let pr_univ l =
     match l with
@@ -168,21 +169,22 @@ let tag_var = tag Tag.variable
 
   let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
 
-  let pr_glob_sort = let open Glob_term in function
-    | UNamed [GSProp,0] -> tag_type (str "SProp")
-    | UNamed [GProp,0] -> tag_type (str "Prop")
-    | UNamed [GSet,0] -> tag_type (str "Set")
+  let pr_sort_expr = function
+    | UNamed [CSProp,0] -> tag_type (str "SProp")
+    | UNamed [CProp,0] -> tag_type (str "Prop")
+    | UNamed [CSet,0] -> tag_type (str "Set")
     | UAnonymous {rigid=true} -> tag_type (str "Type")
     | UAnonymous {rigid=false} -> tag_type (str "Type") ++ pr_univ_annot (fun _ -> str "_") ()
     | UNamed u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u)
 
-  let pr_glob_level = let open Glob_term in function
-    | UNamed GSProp -> tag_type (str "SProp")
-    | UNamed GProp -> tag_type (str "Prop")
-    | UNamed GSet -> tag_type (str "Set")
+  let pr_univ_level_expr = function
+    | UNamed CSProp -> tag_type (str "SProp")
+    | UNamed CProp -> tag_type (str "Prop")
+    | UNamed CSet -> tag_type (str "Set")
     | UAnonymous {rigid=true} -> tag_type (str "Type")
     | UAnonymous {rigid=false} -> tag_type (str "_")
-    | UNamed (GType u) -> tag_type (pr_qualid u)
+    | UNamed (CType u) -> tag_type (pr_qualid u)
+    | UNamed (CRawType s) -> tag_type (Univ.Level.pr s)
 
   let pr_qualid sp =
     let (sl, id) = repr_qualid sp in
@@ -200,7 +202,7 @@ let tag_var = tag Tag.variable
   let pr_patvar = pr_id
 
   let pr_universe_instance l =
-    pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_level)) l
+    pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_univ_level_expr)) l
 
   let pr_reference qid =
     if qualid_is_ident qid then tag_var (pr_id @@ qualid_basename qid)
@@ -664,7 +666,7 @@ let tag_var = tag Tag.variable
       | CPatVar p ->
         return (str "@?" ++ pr_patvar p, latom)
       | CSort s ->
-        return (pr_glob_sort s, latom)
+        return (pr_sort_expr s, latom)
       | CCast (a,b) ->
         return (
           hv 0 (pr mt (LevelLt lcast) a ++ spc () ++
@@ -717,7 +719,7 @@ let tag_var = tag Tag.variable
   let transf env sigma c =
     if !Flags.beautify_file then
       let r = Constrintern.for_grammar (Constrintern.intern_constr env sigma) c in
-      Constrextern.extern_glob_constr (Termops.vars_of_env env) r
+      Constrextern.(extern_glob_constr (extern_env env sigma)) r
     else c
 
   let pr_expr env sigma prec c =
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 02e04573f8..d66b77efb2 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -32,9 +32,9 @@ val pr_id : Id.t -> Pp.t
 val pr_qualid : qualid -> Pp.t
 val pr_patvar : Pattern.patvar -> Pp.t
 
-val pr_glob_sort_name : Glob_term.glob_sort_name -> Pp.t
-val pr_glob_level : Glob_term.glob_level -> Pp.t
-val pr_glob_sort : Glob_term.glob_sort -> Pp.t
+val pr_sort_name_expr : sort_name_expr -> Pp.t
+val pr_univ_level_expr : univ_level_expr -> Pp.t
+val pr_sort_expr : sort_expr -> Pp.t
 val pr_guard_annot
   :  (constr_expr -> Pp.t)
   -> local_binder_expr list
diff --git a/printing/printer.ml b/printing/printer.ml
index ea718526de..1425cebafc 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -97,10 +97,10 @@ let pr_ltype_env ?lax ?goal_concl_style env sigma ?impargs c =
 let pr_ljudge_env env sigma j =
   (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type)
 
-let pr_lglob_constr_env env c =
-  pr_lconstr_expr env (Evd.from_env env) (extern_glob_constr (Termops.vars_of_env env) c)
-let pr_glob_constr_env env c =
-  pr_constr_expr env (Evd.from_env env) (extern_glob_constr (Termops.vars_of_env env) c)
+let pr_lglob_constr_env env sigma c =
+  pr_lconstr_expr env sigma (extern_glob_constr (extern_env env sigma) c)
+let pr_glob_constr_env env sigma c =
+  pr_constr_expr env sigma (extern_glob_constr (extern_env env sigma) c)
 
 let pr_closed_glob_n_env ?lax ?goal_concl_style ?inctx ?scope env sigma n c =
   pr_constr_expr_n env sigma n (extern_closed_glob ?lax ?goal_concl_style ?inctx ?scope env sigma c)
@@ -115,7 +115,7 @@ let pr_constr_pattern_env env sigma c =
 let pr_cases_pattern t =
   pr_cases_pattern_expr (extern_cases_pattern Names.Id.Set.empty t)
 
-let pr_sort sigma s = pr_glob_sort (extern_sort sigma s)
+let pr_sort sigma s = pr_sort_expr (extern_sort sigma s)
 
 let () = Termops.Internal.set_print_constr
   (fun env sigma t -> pr_lconstr_expr env sigma (extern_constr ~lax:true env sigma t))
diff --git a/printing/printer.mli b/printing/printer.mli
index ea388ae57e..732af5570d 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -107,9 +107,9 @@ val pr_closed_glob_env     : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool
 
 val pr_ljudge_env          : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t
 
-val pr_lglob_constr_env      : env -> 'a glob_constr_g -> Pp.t
+val pr_lglob_constr_env    : env -> evar_map -> 'a glob_constr_g -> Pp.t
 
-val pr_glob_constr_env       : env -> 'a glob_constr_g -> Pp.t
+val pr_glob_constr_env     : env -> evar_map -> 'a glob_constr_g -> Pp.t
 
 val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t
 
diff --git a/tactics/declareUctx.ml b/tactics/declareUctx.ml
index 3f67ff20a4..bca43697cb 100644
--- a/tactics/declareUctx.ml
+++ b/tactics/declareUctx.ml
@@ -16,7 +16,7 @@ let name_instance inst =
       assert false
     | Some na ->
       try
-        let qid = Nametab.shortest_qualid_of_universe na in
+        let qid = Nametab.shortest_qualid_of_universe Names.Id.Set.empty na in
         Names.Name (Libnames.qualid_basename qid)
       with Not_found ->
         (* Best-effort naming from the string representation of the level.
diff --git a/test-suite/bugs/closed/bug_13303.v b/test-suite/bugs/closed/bug_13303.v
new file mode 100644
index 0000000000..6bee24b48a
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13303.v
@@ -0,0 +1,27 @@
+Module Pt1.
+
+  Module M. Universe i. End M.
+  Module N. Universe i. End N.
+  Import M.
+  Notation foo := Type@{i (* M.i??? *)}.
+  Import N.
+  Fail Check foo : Type@{M.i}. (* should NOT succeed *)
+  Check foo : Type@{i (* N.i *)}. (* should succeed *)
+
+  Definition bar@{i} := Type@{i}.
+  Check bar : Type@{N.i}.
+  Check bar : Type@{M.i}.
+
+End Pt1.
+
+Module Pt2.
+
+  Module M. Universe i. Notation foo := Type@{i}. End M.
+
+  Definition foo1 := M.foo.
+  (* should succeed, currently errors undeclared universe i *)
+
+  Definition foo2@{i} : Type@{i} := M.foo.
+  (* should succeed, currently errors universe inconsistency *)
+
+End Pt2.
diff --git a/test-suite/misc/quotation_token/src/quotation.mlg b/test-suite/misc/quotation_token/src/quotation.mlg
index ba0bcb1b3c..0f843b3b14 100644
--- a/test-suite/misc/quotation_token/src/quotation.mlg
+++ b/test-suite/misc/quotation_token/src/quotation.mlg
@@ -7,6 +7,6 @@ GRAMMAR EXTEND Gram
   term: LEVEL "0"
     [ [ s = QUOTATION "foobar:" ->
         {
-          CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [GProp,0])) } ] ]
+          CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [CProp,0])) } ] ]
   ;
 END
diff --git a/test-suite/misc/side-eff-leak-univs/src/evil.mlg b/test-suite/misc/side-eff-leak-univs/src/evil.mlg
index d89ab887a8..bb6eaff409 100644
--- a/test-suite/misc/side-eff-leak-univs/src/evil.mlg
+++ b/test-suite/misc/side-eff-leak-univs/src/evil.mlg
@@ -7,7 +7,7 @@ open Stdarg
 
 TACTIC EXTEND magic
 | [ "magic" ident(i) ident(j) ] -> {
-  let open Glob_term in
-  DeclareUniv.do_constraint ~poly:false [ GType (Libnames.qualid_of_ident i), Univ.Lt, GType (Libnames.qualid_of_ident j)]; Proofview.tclUNIT()
+  let open Constrexpr in
+  DeclareUniv.do_constraint ~poly:false [ CType (Libnames.qualid_of_ident i), Univ.Lt, CType (Libnames.qualid_of_ident j)]; Proofview.tclUNIT()
 }
 END
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index d8d3f696b7..0fbb4f4c11 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -1,61 +1,61 @@
-Inductive Empty@{u} : Type@{u} :=  
-(* u |=  *)
-Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A }
-(* u |=  *)
+Inductive Empty@{uu} : Type@{uu} :=  
+(* uu |=  *)
+Record PWrap (A : Type@{uu}) : Type@{uu} := pwrap { punwrap : A }
+(* uu |=  *)
 
 PWrap has primitive projections with eta conversion.
 Arguments PWrap _%type_scope
 Arguments pwrap _%type_scope _
-punwrap@{u} = 
-fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p
-     : forall A : Type@{u}, PWrap@{u} A -> A
-(* u |=  *)
+punwrap@{uu} = 
+fun (A : Type@{uu}) (p : PWrap@{uu} A) => punwrap _ p
+     : forall A : Type@{uu}, PWrap@{uu} A -> A
+(* uu |=  *)
 
 Arguments punwrap _%type_scope _
-Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A }
-(* u |=  *)
+Record RWrap (A : Type@{uu}) : Type@{uu} := rwrap { runwrap : A }
+(* uu |=  *)
 
 Arguments RWrap _%type_scope
 Arguments rwrap _%type_scope _
-runwrap@{u} = 
-fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap
-     : forall A : Type@{u}, RWrap@{u} A -> A
-(* u |=  *)
+runwrap@{uu} = 
+fun (A : Type@{uu}) (r : RWrap@{uu} A) => let (runwrap) := r in runwrap
+     : forall A : Type@{uu}, RWrap@{uu} A -> A
+(* uu |=  *)
 
 Arguments runwrap _%type_scope _
-Wrap@{u} = fun A : Type@{u} => A
-     : Type@{u} -> Type@{u}
-(* u |=  *)
+Wrap@{uu} = fun A : Type@{uu} => A
+     : Type@{uu} -> Type@{uu}
+(* uu |=  *)
 
 Arguments Wrap _%type_scope
-wrap@{u} = 
-fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap
-     : forall A : Type@{u}, Wrap@{u} A -> A
-(* u |=  *)
+wrap@{uu} = 
+fun (A : Type@{uu}) (Wrap : Wrap@{uu} A) => Wrap
+     : forall A : Type@{uu}, Wrap@{uu} A -> A
+(* uu |=  *)
 
 Arguments wrap {A}%type_scope {Wrap}
-bar@{u} = nat
-     : Wrap@{u} Set
-(* u |= Set < u *)
-foo@{u u0 v} = 
-Type@{u0} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1,u0+1,v+1)}
-(* u u0 v |=  *)
+bar@{uu} = nat
+     : Wrap@{uu} Set
+(* uu |= Set < uu *)
+foo@{uu u v} = 
+Type@{u} -> Type@{v} -> Type@{uu}
+     : Type@{max(uu+1,u+1,v+1)}
+(* uu u v |=  *)
 Type@{i} -> Type@{j}
      : Type@{max(i+1,j+1)}
 (* {j i} |=  *)
      = Type@{i} -> Type@{j}
      : Type@{max(i+1,j+1)}
 (* {j i} |=  *)
-mono = Type@{mono.u}
-     : Type@{mono.u+1}
-(* {mono.u} |=  *)
+mono = Type@{mono.uu}
+     : Type@{mono.uu+1}
+(* {mono.uu} |=  *)
 mono
-     : Type@{mono.u+1}
-Type@{mono.u}
-     : Type@{mono.u+1}
+     : Type@{mono.uu+1}
+Type@{mono.uu}
+     : Type@{mono.uu+1}
 The command has indeed failed with message:
-Universe u already exists.
+Universe uu already exists.
 monomono
      : Type@{MONOU+1}
 mono.monomono
@@ -63,23 +63,23 @@ mono.monomono
 monomono
      : Type@{MONOU+1}
 mono
-     : Type@{mono.u+1}
+     : Type@{mono.uu+1}
 The command has indeed failed with message:
-Universe u already exists.
+Universe uu already exists.
 bobmorane = 
 let tt := Type@{UnivBinders.32} in
 let ff := Type@{UnivBinders.34} in tt -> ff
      : Type@{max(UnivBinders.31,UnivBinders.33)}
 The command has indeed failed with message:
-Universe u already bound.
+Universe uu already bound.
 foo@{E M N} = 
 Type@{M} -> Type@{N} -> Type@{E}
      : Type@{max(E+1,M+1,N+1)}
 (* E M N |=  *)
-foo@{u u0 v} = 
-Type@{u0} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1,u0+1,v+1)}
-(* u u0 v |=  *)
+foo@{uu u v} = 
+Type@{u} -> Type@{v} -> Type@{uu}
+     : Type@{max(uu+1,u+1,v+1)}
+(* uu u v |=  *)
 Inductive Empty@{E} : Type@{E} :=  
 (* E |=  *)
 Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }
@@ -103,45 +103,38 @@ The command has indeed failed with message:
 This object does not support universe names.
 The command has indeed failed with message:
 Cannot enforce v < u because u < gU < gV < v
-bind_univs.mono = 
-Type@{bind_univs.mono.u}
-     : Type@{bind_univs.mono.u+1}
-(* {bind_univs.mono.u} |=  *)
-bind_univs.poly@{u} = Type@{u}
-     : Type@{u+1}
-(* u |=  *)
-insec@{v} = Type@{u} -> Type@{v}
-     : Type@{max(u+1,v+1)}
+insec@{v} = Type@{uu} -> Type@{v}
+     : Type@{max(uu+1,v+1)}
 (* v |=  *)
 Inductive insecind@{k} : Type@{k+1} :=
     inseccstr : Type@{k} -> insecind@{k}
 (* k |=  *)
 
 Arguments inseccstr _%type_scope
-insec@{u v} = Type@{u} -> Type@{v}
-     : Type@{max(u+1,v+1)}
-(* u v |=  *)
-Inductive insecind@{u k} : Type@{k+1} :=
-    inseccstr : Type@{k} -> insecind@{u k}
-(* u k |=  *)
+insec@{uu v} = Type@{uu} -> Type@{v}
+     : Type@{max(uu+1,v+1)}
+(* uu v |=  *)
+Inductive insecind@{uu k} : Type@{k+1} :=
+    inseccstr : Type@{k} -> insecind@{uu k}
+(* uu k |=  *)
 
 Arguments inseccstr _%type_scope
 insec2@{u} = Prop
      : Type@{Set+1}
 (* u |=  *)
-inmod@{u} = Type@{u}
-     : Type@{u+1}
-(* u |=  *)
-SomeMod.inmod@{u} = Type@{u}
-     : Type@{u+1}
-(* u |=  *)
-inmod@{u} = Type@{u}
-     : Type@{u+1}
-(* u |=  *)
-Applied.infunct@{u v} = 
-inmod@{u} -> Type@{v}
-     : Type@{max(u+1,v+1)}
-(* u v |=  *)
+inmod@{uu} = Type@{uu}
+     : Type@{uu+1}
+(* uu |=  *)
+SomeMod.inmod@{uu} = Type@{uu}
+     : Type@{uu+1}
+(* uu |=  *)
+inmod@{uu} = Type@{uu}
+     : Type@{uu+1}
+(* uu |=  *)
+Applied.infunct@{uu v} = 
+inmod@{uu} -> Type@{v}
+     : Type@{max(uu+1,v+1)}
+(* uu v |=  *)
 axfoo@{i u u0} : Type@{u} -> Type@{i}
 (* i u u0 |=  *)
 
@@ -166,3 +159,13 @@ Arguments axbar' _%type_scope
 Expands to: Constant UnivBinders.axbar'
 The command has indeed failed with message:
 When declaring multiple axioms in one command, only the first is allowed a universe binder (which will be shared by the whole block).
+foo@{i} = Type@{M.i} -> Type@{i}
+     : Type@{max(M.i+1,i+1)}
+(* i |=  *)
+bind_univs.mono = 
+Type@{bind_univs.mono.u}
+     : Type@{bind_univs.mono.u+1}
+(* {bind_univs.mono.u} |=  *)
+bind_univs.poly@{u} = Type@{u}
+     : Type@{u+1}
+(* u |=  *)
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 582a5e969a..ed6e90b2a6 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -5,32 +5,32 @@ Set Printing Universes.
 (* Unset Strict Universe Declaration. *)
 
 (* universe binders on inductive types and record projections *)
-Inductive Empty@{u} : Type@{u} := .
+Inductive Empty@{uu} : Type@{uu} := .
 Print Empty.
 
 Set Primitive Projections.
-Record PWrap@{u} (A:Type@{u}) := pwrap { punwrap : A }.
+Record PWrap@{uu} (A:Type@{uu}) := pwrap { punwrap : A }.
 Print PWrap.
 Print punwrap.
 
 Unset Primitive Projections.
-Record RWrap@{u} (A:Type@{u}) := rwrap { runwrap : A }.
+Record RWrap@{uu} (A:Type@{uu}) := rwrap { runwrap : A }.
 Print RWrap.
 Print runwrap.
 
 (* universe binders also go on the constants for operational typeclasses. *)
-Class Wrap@{u} (A:Type@{u}) := wrap : A.
+Class Wrap@{uu} (A:Type@{uu}) := wrap : A.
 Print Wrap.
 Print wrap.
 
 (* Instance in lemma mode used to ignore the binders. *)
-Instance bar@{u} : Wrap@{u} Set. Proof. exact nat. Qed.
+Instance bar@{uu} : Wrap@{uu} Set. Proof. exact nat. Qed.
 Print bar.
 
 Unset Strict Universe Declaration.
 (* The universes in the binder come first, then the extra universes in
    order of appearance. *)
-Definition foo@{u +} := Type -> Type@{v} -> Type@{u}.
+Definition foo@{uu +} := Type -> Type@{v} -> Type@{uu}.
 Print foo.
 
 Check Type@{i} -> Type@{j}.
@@ -40,13 +40,13 @@ Eval cbv in Type@{i} -> Type@{j}.
 Set Strict Universe Declaration.
 
 (* Binders even work with monomorphic definitions! *)
-Monomorphic Definition mono@{u} := Type@{u}.
+Monomorphic Definition mono@{uu} := Type@{uu}.
 Print mono.
 Check mono.
-Check Type@{mono.u}.
+Check Type@{mono.uu}.
 
 Module mono.
-  Fail Monomorphic Universe u.
+  Fail Monomorphic Universe uu.
   Monomorphic Universe MONOU.
 
   Monomorphic Definition monomono := Type@{MONOU}.
@@ -60,28 +60,28 @@ Import mono.
 Check monomono. (* unqualified MONOU *)
 Check mono. (* still qualified mono.u *)
 
-Monomorphic Constraint Set < UnivBinders.mono.u.
+Monomorphic Constraint Set < UnivBinders.mono.uu.
 
 Module mono2.
-  Monomorphic Universe u.
+  Monomorphic Universe uu.
 End mono2.
 
-Fail Monomorphic Definition mono2@{u} := Type@{u}.
+Fail Monomorphic Definition mono2@{uu} := Type@{uu}.
 
 Module SecLet.
   Unset Universe Polymorphism.
   Section foo.
-    (* Fail Let foo@{} := Type@{u}. (* doesn't parse: Let foo@{...} doesn't exist *) *)
+    (* Fail Let foo@{} := Type@{uu}. (* doesn't parse: Let foo@{...} doesn't exist *) *)
     Unset Strict Universe Declaration.
-    Let tt : Type@{u} := Type@{v}. (* names disappear in the ether *)
-    Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* names disappear into space *)
+    Let tt : Type@{uu} := Type@{v}. (* names disappear in the ether *)
+    Let ff : Type@{uu}. Proof. exact Type@{v}. Qed. (* names disappear into space *)
     Definition bobmorane := tt -> ff.
   End foo.
   Print bobmorane.
 End SecLet.
 
 (* fun x x => foo is nonsense with local binders *)
-Fail Definition fo@{u u} := Type@{u}.
+Fail Definition fo@{uu uu} := Type@{uu}.
 
 (* Using local binders for printing. *)
 Print foo@{E M N}.
@@ -106,14 +106,9 @@ Fail Print Coq.Init.Logic@{E}.
 Monomorphic Universes gU gV. Monomorphic Constraint gU < gV.
 Fail Lemma foo@{u v|u < gU, gV < v, v < u} : nat.
 
-(* Universe binders survive through compilation, sections and modules. *)
-Require TestSuite.bind_univs.
-Print bind_univs.mono.
-Print bind_univs.poly.
-
 Section SomeSec.
-  Universe u.
-  Definition insec@{v} := Type@{u} -> Type@{v}.
+  Universe uu.
+  Definition insec@{v} := Type@{uu} -> Type@{v}.
   Print insec.
 
   Inductive insecind@{k} := inseccstr : Type@{k} -> insecind.
@@ -129,7 +124,7 @@ End SomeSec2.
 Print insec2.
 
 Module SomeMod.
-  Definition inmod@{u} := Type@{u}.
+  Definition inmod@{uu} := Type@{uu}.
   Print inmod.
 End SomeMod.
 Print SomeMod.inmod.
@@ -138,7 +133,7 @@ Print inmod.
 
 Module Type SomeTyp. Definition inmod := Type. End SomeTyp.
 Module SomeFunct (In : SomeTyp).
-  Definition infunct@{u v} := In.inmod@{u} -> Type@{v}.
+  Definition infunct@{uu v} := In.inmod@{uu} -> Type@{v}.
 End SomeFunct.
 Module Applied := SomeFunct(SomeMod).
 Print Applied.infunct.
@@ -147,7 +142,7 @@ Print Applied.infunct.
 
    In polymorphic mode the domain Type gets separate universes for the
    different axioms, but all axioms have to declare all universes. In
-   polymorphic mode they get the same universes, ie the type is only
+   monomorphic mode they get the same universes, ie the type is only
    interpd once. *)
 Axiom axfoo@{i+} axbar : Type -> Type@{i}.
 Monomorphic Axiom axfoo'@{i+} axbar' : Type -> Type@{i}.
@@ -155,3 +150,18 @@ Monomorphic Axiom axfoo'@{i+} axbar' : Type -> Type@{i}.
 About axfoo. About axbar. About axfoo'. About axbar'.
 
 Fail Axiom failfoo failbar@{i} : Type.
+
+(* Notation interaction *)
+Module Notas.
+  Unset Universe Polymorphism.
+  Module Import M. Universe i. End M.
+
+  Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}.
+  Print foo. (* must not print Type@{i} -> Type@{i} *)
+
+End Notas.
+
+(* Universe binders survive through compilation, sections and modules. *)
+Require TestSuite.bind_univs.
+Print bind_univs.mono.
+Print bind_univs.poly.
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 5d49d1635c..01b1025da1 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1100,7 +1100,7 @@ let interp_constr flags ist c =
 let () =
   let intern = intern_constr in
   let interp ist c = interp_constr constr_flags ist c in
-  let print env c = str "constr:(" ++ Printer.pr_lglob_constr_env env c ++ str ")" in
+  let print env sigma c = str "constr:(" ++ Printer.pr_lglob_constr_env env sigma c ++ str ")" in
   let subst subst c = Detyping.subst_glob_constr (Global.env()) subst c in
   let obj = {
     ml_intern = intern;
@@ -1113,7 +1113,7 @@ let () =
 let () =
   let intern = intern_constr in
   let interp ist c = interp_constr open_constr_no_classes_flags ist c in
-  let print env c = str "open_constr:(" ++ Printer.pr_lglob_constr_env env c ++ str ")" in
+  let print env sigma c = str "open_constr:(" ++ Printer.pr_lglob_constr_env env sigma c ++ str ")" in
   let subst subst c = Detyping.subst_glob_constr (Global.env()) subst c in
   let obj = {
     ml_intern = intern;
@@ -1125,7 +1125,7 @@ let () =
 
 let () =
   let interp _ id = return (Value.of_ident id) in
-  let print _ id = str "ident:(" ++ Id.print id ++ str ")" in
+  let print _ _ id = str "ident:(" ++ Id.print id ++ str ")" in
   let obj = {
     ml_intern = (fun _ _ id -> GlbVal id, gtypref t_ident);
     ml_interp = interp;
@@ -1147,7 +1147,7 @@ let () =
     let sigma = Evd.from_env env in
     Patternops.subst_pattern env sigma subst c
   in
-  let print env pat = str "pattern:(" ++ Printer.pr_lconstr_pattern_env env Evd.empty pat ++ str ")" in
+  let print env sigma pat = str "pattern:(" ++ Printer.pr_lconstr_pattern_env env sigma pat ++ str ")" in
   let interp _ c = return (Value.of_pattern c) in
   let obj = {
     ml_intern = intern;
@@ -1169,7 +1169,7 @@ let () =
     return (Value.of_ext val_preterm c)
   in
   let subst subst c = Detyping.subst_glob_constr (Global.env()) subst c in
-  let print env c = str "preterm:(" ++ Printer.pr_lglob_constr_env env c ++ str ")" in
+  let print env sigma c = str "preterm:(" ++ Printer.pr_lglob_constr_env env sigma c ++ str ")" in
   let obj = {
     ml_intern = (fun _ _ e -> Empty.abort e);
     ml_interp = interp;
@@ -1193,7 +1193,7 @@ let () =
   in
   let subst s c = Globnames.subst_global_reference s c in
   let interp _ gr = return (Value.of_reference gr) in
-  let print _ = function
+  let print _ _ = function
   | GlobRef.VarRef id -> str "reference:(" ++ str "&" ++ Id.print id ++ str ")"
   | r -> str "reference:(" ++ Printer.pr_global r ++ str ")"
   in
@@ -1241,7 +1241,7 @@ let () =
       return (Tac2ffi.of_closure (Tac2ffi.abstract len clos))
   in
   let subst s (ids, tac) = (ids, Genintern.substitute Ltac_plugin.Tacarg.wit_tactic s tac) in
-  let print env (ids, tac) =
+  let print env sigma (ids, tac) =
     let ids =
       if List.is_empty ids then mt ()
       else pr_sequence Id.print ids ++ spc () ++ str "|-" ++ spc ()
@@ -1290,7 +1290,7 @@ let () =
       return (Tac2ffi.of_closure (Tac2ffi.abstract len clos))
   in
   let subst s (ids, tac) = (ids, Genintern.substitute Tacarg.wit_tactic s tac) in
-  let print env (ids, tac) =
+  let print env sigma (ids, tac) =
     let ids =
       if List.is_empty ids then mt ()
       else pr_sequence Id.print ids ++ str " |- "
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index eebd6635fa..d0655890a7 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -853,8 +853,10 @@ let pr_frame = function
   str "Prim <" ++ str ml.mltac_plugin ++ str ":" ++ str ml.mltac_tactic ++ str ">"
 | FrExtn (tag, arg) ->
   let obj = Tac2env.interp_ml_object tag in
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
   str "Extn " ++ str (Tac2dyn.Arg.repr tag) ++ str ":" ++ spc () ++
-    obj.Tac2env.ml_print (Global.env ()) arg
+    obj.Tac2env.ml_print env sigma arg
 
 let () = register_handler begin function
 | Tac2interp.LtacError (kn, args) ->
diff --git a/user-contrib/Ltac2/tac2env.ml b/user-contrib/Ltac2/tac2env.ml
index 6c2133f8f2..f6d07e484b 100644
--- a/user-contrib/Ltac2/tac2env.ml
+++ b/user-contrib/Ltac2/tac2env.ml
@@ -253,7 +253,7 @@ type ('a, 'b) ml_object = {
   ml_intern : 'r. (raw_tacexpr, glb_tacexpr, 'r) intern_fun -> ('a, 'b or_glb_tacexpr, 'r) intern_fun;
   ml_subst : Mod_subst.substitution -> 'b -> 'b;
   ml_interp : environment -> 'b -> valexpr Proofview.tactic;
-  ml_print : Environ.env -> 'b -> Pp.t;
+  ml_print : Environ.env -> Evd.evar_map -> 'b -> Pp.t;
 }
 
 module MLTypeObj =
diff --git a/user-contrib/Ltac2/tac2env.mli b/user-contrib/Ltac2/tac2env.mli
index 2468959810..af1197c24c 100644
--- a/user-contrib/Ltac2/tac2env.mli
+++ b/user-contrib/Ltac2/tac2env.mli
@@ -122,7 +122,7 @@ type ('a, 'b) ml_object = {
   ml_intern : 'r. (raw_tacexpr, glb_tacexpr, 'r) intern_fun -> ('a, 'b or_glb_tacexpr, 'r) intern_fun;
   ml_subst : Mod_subst.substitution -> 'b -> 'b;
   ml_interp : environment -> 'b -> valexpr Proofview.tactic;
-  ml_print : Environ.env -> 'b -> Pp.t;
+  ml_print : Environ.env -> Evd.evar_map -> 'b -> Pp.t;
 }
 
 val define_ml_object : ('a, 'b) Tac2dyn.Arg.tag -> ('a, 'b) ml_object -> unit
diff --git a/user-contrib/Ltac2/tac2print.ml b/user-contrib/Ltac2/tac2print.ml
index a37fe2f7a5..fe62de1fb3 100644
--- a/user-contrib/Ltac2/tac2print.ml
+++ b/user-contrib/Ltac2/tac2print.ml
@@ -274,7 +274,9 @@ let pr_glbexpr_gen lvl c =
     paren (hov 0 (c ++ spc () ++ (pr_sequence (pr_glbexpr E0) cl)))
   | GTacExt (tag, arg) ->
     let tpe = interp_ml_object tag in
-    hov 0 (tpe.ml_print (Global.env ()) arg) (* FIXME *)
+    let env = Global.env() in
+    let sigma = Evd.from_env env in
+    hov 0 (tpe.ml_print env sigma arg) (* FIXME *)
   | GTacPrm (prm, args) ->
     let args = match args with
     | [] -> mt ()
diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml
index 1705915e70..1987d48e0f 100644
--- a/vernac/declareUniv.ml
+++ b/vernac/declareUniv.ml
@@ -109,9 +109,8 @@ let do_universe ~poly l =
 
 let do_constraint ~poly l =
   let open Univ in
-  let u_of_id x =
-    Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x
-  in
+  let evd = Evd.from_env (Global.env ()) in
+  let u_of_id x = Constrintern.interp_known_level evd x in
   let constraints = List.fold_left (fun acc (l, d, r) ->
       let lu = u_of_id l and ru = u_of_id r in
       Constraint.add (lu, d, ru) acc)
diff --git a/vernac/declareUniv.mli b/vernac/declareUniv.mli
index e4d1d5dc65..ca990a58eb 100644
--- a/vernac/declareUniv.mli
+++ b/vernac/declareUniv.mli
@@ -17,4 +17,4 @@ exception AlreadyDeclared of (string option * Id.t)
 val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
 
 val do_universe : poly:bool -> lident list -> unit
-val do_constraint : poly:bool -> Glob_term.glob_constraint list -> unit
+val do_constraint : poly:bool -> Constrexpr.univ_constraint_expr list -> unit
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 777b3b0c96..d35e13c4ef 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -968,7 +968,7 @@ let explain_not_match_error = function
         status (not b) ++ str" declaration was found"
   | IncompatibleUniverses incon ->
     str"the universe constraints are inconsistent: " ++
-      Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes incon
+      Univ.explain_universe_inconsistency UnivNames.(pr_with_global_universes empty_binders) incon
   | IncompatiblePolymorphism (env, t1, t2) ->
     str "conversion of polymorphic values generates additional constraints: " ++
       quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t1) ++ spc () ++
@@ -1225,7 +1225,7 @@ let error_large_non_prop_inductive_not_in_type () =
   str "Large non-propositional inductive types must be in Type."
 
 let error_inductive_missing_constraints (us,ind_univ) =
-  let pr_u = Univ.Universe.pr_with UnivNames.pr_with_global_universes in
+  let pr_u = Univ.Universe.pr_with UnivNames.(pr_with_global_universes empty_binders) in
   str "Missing universe constraint declared for inductive type:" ++ spc()
   ++ v 0 (prlist_with_sep spc (fun u ->
       hov 0 (pr_u u ++ str " <= " ++ pr_u ind_univ))
@@ -1413,7 +1413,7 @@ let _ = CErrors.register_handler (wrap_unhandled explain_exn_default)
 let rec vernac_interp_error_handler = function
   | Univ.UniverseInconsistency i ->
     str "Universe inconsistency." ++ spc() ++
-    Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i ++ str "."
+    Univ.explain_universe_inconsistency UnivNames.(pr_with_global_universes empty_binders) i ++ str "."
   | TypeError(ctx,te) ->
     let te = map_ptype_error EConstr.of_constr te in
     explain_type_error ctx Evd.empty te
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 01873918aa..ff4365c8d3 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -60,8 +60,8 @@ let pr_red_expr =
     keyword
 
 let pr_uconstraint (l, d, r) =
-  pr_glob_sort_name l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
-  pr_glob_sort_name r
+  pr_sort_name_expr l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
+  pr_sort_name_expr r
 
 let pr_univ_name_list = function
   | None -> mt ()
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 840754ccc6..0fc6c7f87b 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -206,7 +206,7 @@ let print_if_is_coercion ref =
 
 let pr_template_variables = function
   | [] -> mt ()
-  | vars -> str "on " ++ prlist_with_sep spc UnivNames.pr_with_global_universes vars
+  | vars -> str "on " ++ prlist_with_sep spc UnivNames.(pr_with_global_universes empty_binders) vars
 
 let print_polymorphism ref =
   let poly = Global.is_polymorphic ref in
@@ -668,7 +668,7 @@ let gallina_print_syntactic_def env kn =
         spc () ++ str ":=") ++
      spc () ++
      Constrextern.without_specific_symbols
-       [Notation.SynDefRule kn] (pr_glob_constr_env env) c)
+       [Notation.SynDefRule kn] (pr_glob_constr_env env (Evd.from_env env)) c)
 
 module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> Pp.t option end)
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 0f63dfe5ce..57b264bbc2 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -353,9 +353,9 @@ let universe_subgraph ?loc kept univ =
   let open Univ in
   let sigma = Evd.from_env (Global.env()) in
   let parse q =
-    let q =  Glob_term.(GType q) in
+    let q = Constrexpr.CType q in
     (* this function has a nice error message for not found univs *)
-    Pretyping.interp_known_glob_level ?loc sigma q
+    Constrintern.interp_known_level sigma q
   in
   let kept = List.fold_left (fun kept q -> LSet.add (parse q) kept) LSet.empty kept in
   let csts = UGraph.constraints_for ~kept univ in
@@ -377,7 +377,7 @@ let print_universes ?loc ~sort ~subgraph dst =
     if Global.is_joined_environment () then mt ()
     else str"There may remain asynchronous universe constraints"
   in
-  let prl = UnivNames.pr_with_global_universes in
+  let prl = UnivNames.(pr_with_global_universes empty_binders) in
   begin match dst with
     | None -> UGraph.pr_universes prl univ ++ pr_remaining
     | Some s -> dump_universes_gen (fun u -> Pp.string_of_ppcmds (prl u)) univ s
@@ -1829,11 +1829,11 @@ let vernac_print ~pstate =
   | PrintHintDbName s -> Hints.pr_hint_db_by_name env sigma s
   | PrintHintDb -> Hints.pr_searchtable env sigma
   | PrintScopes ->
-    Notation.pr_scopes (Constrextern.without_symbols (pr_glob_constr_env env))
+    Notation.pr_scopes (Constrextern.without_symbols (pr_glob_constr_env env sigma))
   | PrintScope s ->
-    Notation.pr_scope (Constrextern.without_symbols (pr_glob_constr_env env)) s
+    Notation.pr_scope (Constrextern.without_symbols (pr_glob_constr_env env sigma)) s
   | PrintVisibility s ->
-    Notation.pr_visibility (Constrextern.without_symbols (pr_glob_constr_env env)) s
+    Notation.pr_visibility (Constrextern.without_symbols (pr_glob_constr_env env sigma)) s
   | PrintAbout (ref_or_by_not,udecl,glnumopt) ->
     print_about_hyp_globs ~pstate ref_or_by_not udecl glnumopt
   | PrintImplicit qid ->
@@ -1867,9 +1867,9 @@ let vernac_locate ~pstate = let open Constrexpr in function
   | LocateTerm {v=AN qid} -> Prettyp.print_located_term qid
   | LocateAny {v=ByNotation (ntn, sc)} (* TODO : handle Ltac notations *)
   | LocateTerm {v=ByNotation (ntn, sc)} ->
-    let _, env = get_current_or_global_context ~pstate in
+    let sigma, env = get_current_or_global_context ~pstate in
     Notation.locate_notation
-      (Constrextern.without_symbols (pr_glob_constr_env env)) ntn sc
+      (Constrextern.without_symbols (pr_glob_constr_env env sigma)) ntn sc
   | LocateLibrary qid -> print_located_library qid
   | LocateModule qid -> Prettyp.print_located_module qid
   | LocateOther (s, qid) -> Prettyp.print_located_other s qid
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index defb0691c0..2e360cf969 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -129,8 +129,6 @@ type option_setting =
 
 (** Identifier and optional list of bound universes and constraints. *)
 
-type sort_expr = Sorts.family
-
 type definition_expr =
   | ProveBody of local_binder_expr list * constr_expr
   | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr
@@ -210,8 +208,8 @@ type proof_end =
   | Proved of opacity_flag * lident option
 
 type scheme =
-  | InductionScheme of bool * qualid or_by_notation * sort_expr
-  | CaseScheme of bool * qualid or_by_notation * sort_expr
+  | InductionScheme of bool * qualid or_by_notation * Sorts.family
+  | CaseScheme of bool * qualid or_by_notation * Sorts.family
   | EqualityScheme of qualid or_by_notation
 
 type section_subset_expr =
@@ -341,7 +339,7 @@ type nonrec vernac_expr =
   | VernacScheme of (lident option * scheme) list
   | VernacCombinedScheme of lident * lident list
   | VernacUniverse of lident list
-  | VernacConstraint of Glob_term.glob_constraint list
+  | VernacConstraint of univ_constraint_expr list
 
   (* Gallina extensions *)
   | VernacBeginSection of lident