Separate interning and pretyping of universes

This allows proper treatment in notations, ie fixes #13303

The "glob" representation of universes (what pretyping sees) contains
only fully interpreted (kernel) universes and unbound universe
ids (for non Strict Universe Declaration).

This means universes need to be understood at intern time, so intern
now has a new "universe binders" argument. We cannot avoid this due to
the following example:

~~~coq
Module Import M. Universe i. End M.
Definition foo@{i} := Type@{i}.
~~~

When interning `Type@{i}` we need to know that `i` is locally bound to
avoid interning it as `M.i`.

Extern has a symmetrical problem:

~~~coq
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} *)
~~~
(Polymorphic as otherwise the local `i` will be called `foo.i`)

Therefore extern also takes a universe binders argument.

Note that the current implementation actually replaces local universes
with names at detype type. (Asymmetrical to pretyping which only gets
names in glob terms for dynamically declared univs, although it's
capable of understanding bound univs too)

As such extern only really needs the domain of the universe
binders (ie the set of bound universe ids), we just arbitrarily pass
the whole universe binders to avoid putting `Id.Map.domain` at every
entry point.

Note that if we want to change so that detyping does not name locally
bound univs we would need to pass the reverse universe binders (map
from levels to ids, contained in the ustate ie in the evar map) to
extern.

7 files changed, 205 insertions, 84 deletions

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