Merge PR #13415: Separate interning and pretyping of universes

Reviewed-by: mattam82

7 files changed, 21 insertions, 24 deletions

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