Safe API for accessing universe constraints of global references.

Instead of returning either an instance or the set of constraints, we rather
return the corresponding abstracted context. We also push back all uses of
abstraction-breaking calls from these functions out of the kernel.

18 files changed, 67 insertions, 97 deletions

diff --git a/checker/inductive.ml b/checker/inductive.ml
index a145165aa..1271a02b0 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -66,13 +66,6 @@ let inductive_is_cumulative mib =
   | Polymorphic_ind ctx -> false
   | Cumulative_ind cumi -> true
 
-let inductive_polymorphic_context mib =
-  match mib.mind_universes with
-  | Monomorphic_ind _ -> Univ.UContext.empty
-  | Polymorphic_ind ctx -> Univ.instantiate_univ_context ctx
-  | Cumulative_ind cumi -> 
-    Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi)
-
 (************************************************************************)
 
 (* Build the substitution that replaces Rels by the appropriate *)
diff --git a/checker/inductive.mli b/checker/inductive.mli
index b8cbda7cf..8f605935d 100644
--- a/checker/inductive.mli
+++ b/checker/inductive.mli
@@ -26,8 +26,6 @@ val inductive_is_polymorphic : mutual_inductive_body -> bool
 
 val inductive_is_cumulative : mutual_inductive_body -> bool
 
-val inductive_polymorphic_context : mutual_inductive_body -> Univ.universe_context
-
 val type_of_inductive : env -> mind_specif puniverses -> constr
 
 (* Return type as quoted by the user *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 1337036b8..cf6d3c55e 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -67,24 +67,14 @@ let type_of_constant cb =
       if t' == t then x else RegularArity t'
   | TemplateArity _ as x -> x
 
-let universes_of_polymorphic_constant otab cb = 
-  match cb.const_universes with
-  | Monomorphic_const _ -> Univ.UContext.empty
-  | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx
-
 let constant_has_body cb = match cb.const_body with
   | Undef _ -> false
   | Def _ | OpaqueDef _ -> true
 
-let constant_polymorphic_instance cb =
-  match cb.const_universes with
-  | Monomorphic_const _ -> Univ.Instance.empty
-  | Polymorphic_const ctx -> Univ.AUContext.instance ctx
-
 let constant_polymorphic_context cb =
   match cb.const_universes with
-  | Monomorphic_const _ -> Univ.UContext.empty
-  | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx
+  | Monomorphic_const _ -> Univ.AUContext.empty
+  | Polymorphic_const ctx -> ctx
 
 let is_opaque cb = match cb.const_body with
   | OpaqueDef _ -> true
@@ -268,19 +258,11 @@ let subst_mind_body sub mib =
     mind_typing_flags = mib.mind_typing_flags;
   }
 
-let inductive_polymorphic_instance mib =
-  match mib.mind_universes with
-  | Monomorphic_ind _ -> Univ.Instance.empty
-  | Polymorphic_ind ctx -> Univ.AUContext.instance ctx
-  | Cumulative_ind cumi -> 
-    Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)
-
 let inductive_polymorphic_context mib =
   match mib.mind_universes with
-  | Monomorphic_ind _ -> Univ.UContext.empty
-  | Polymorphic_ind ctx -> Univ.instantiate_univ_context ctx
-  | Cumulative_ind cumi -> 
-    Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi)
+  | Monomorphic_ind _ -> Univ.AUContext.empty
+  | Polymorphic_ind ctx -> ctx
+  | Cumulative_ind cumi -> Univ.ACumulativityInfo.univ_context cumi
 
 let inductive_is_polymorphic mib =
   match mib.mind_universes with
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 7350724b8..987c1adaf 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -27,8 +27,7 @@ val subst_const_body : substitution -> constant_body -> constant_body
 
 val constant_has_body : constant_body -> bool
 
-val constant_polymorphic_instance : constant_body -> universe_instance
-val constant_polymorphic_context : constant_body -> universe_context
+val constant_polymorphic_context : constant_body -> abstract_universe_context
 
 (** Is the constant polymorphic? *)
 val constant_is_polymorphic : constant_body -> bool
@@ -43,9 +42,6 @@ val type_of_constant : constant_body -> constant_type
 (** Return the universe context, in case the definition is polymorphic, otherwise
     the context is empty. *)
 
-val universes_of_polymorphic_constant :
-  Opaqueproof.opaquetab -> constant_body -> Univ.universe_context
-
 val is_opaque : constant_body -> bool
 
 (** Side effects *)
@@ -68,8 +64,7 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
 
 val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body
 
-val inductive_polymorphic_instance : mutual_inductive_body -> universe_instance
-val inductive_polymorphic_context : mutual_inductive_body -> universe_context
+val inductive_polymorphic_context : mutual_inductive_body -> abstract_universe_context
 
 (** Is the inductive polymorphic? *)
 val inductive_is_polymorphic : mutual_inductive_body -> bool
diff --git a/kernel/environ.ml b/kernel/environ.ml
index ca2c8e135..b01b65200 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -247,17 +247,11 @@ let constant_type env (kn,u) =
     let csts = constraints_of cb u in
     (map_regular_arity (subst_instance_constr u) cb.const_type, csts)
 
-let constant_instance env kn =
-  let cb = lookup_constant kn env in
-  match cb.const_universes with
-  | Monomorphic_const _ -> Univ.Instance.empty
-  | Polymorphic_const ctx -> Univ.AUContext.instance ctx
-
 let constant_context env kn =
   let cb = lookup_constant kn env in
   match cb.const_universes with
-  | Monomorphic_const _ -> Univ.UContext.empty
-  | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx
+  | Monomorphic_const _ -> Univ.AUContext.empty
+  | Polymorphic_const ctx -> ctx
 
 type const_evaluation_result = NoBody | Opaque | IsProj
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index f8887d8e8..cd7a9d279 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -160,10 +160,7 @@ val constant_value_and_type : env -> constant puniverses ->
   constr option * constant_type * Univ.constraints
 (** The universe context associated to the constant, empty if not 
     polymorphic *)
-val constant_context : env -> constant -> Univ.universe_context
-(** The universe isntance associated to the constant, empty if not 
-    polymorphic *)
-val constant_instance : env -> constant -> Univ.universe_instance
+val constant_context : env -> constant -> Univ.abstract_universe_context
 
 (* These functions should be called under the invariant that [env] 
    already contains the constraints corresponding to the constant 
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 9d7262206..da7fcd6f2 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1959,14 +1959,14 @@ let param_name = Name (id_of_string "params")
 let arg_name = Name (id_of_string "arg")
 
 let compile_mind prefix ~interactive mb mind stack =
-  let u = Declareops.inductive_polymorphic_instance mb in
+  let u = Declareops.inductive_polymorphic_context mb in
   let f i stack ob =
     let gtype = Gtype((mind, i), Array.map snd ob.mind_reloc_tbl) in
     let j = push_symbol (SymbInd (mind,i)) in
     let name = Gind ("", (mind, i)) in
     let accu =
       let args =
-	if Univ.Instance.is_empty u then
+	if Int.equal (Univ.AUContext.size u) 0 then
 	  [|get_ind_code j; MLarray [||]|]
 	else [|get_ind_code j|]
       in
diff --git a/library/global.ml b/library/global.ml
index 8b59c84dd..09c202c50 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -164,49 +164,49 @@ let type_of_global_unsafe r =
   match r with
   | VarRef id -> Environ.named_type id env
   | ConstRef c -> 
-     let cb = Environ.lookup_constant c env in 
-     let univs =
-       Declareops.universes_of_polymorphic_constant
-         (Environ.opaque_tables env) cb in
-     let ty = Typeops.type_of_constant_type env cb.Declarations.const_type in
-       Vars.subst_instance_constr (Univ.UContext.instance univs) ty
+    let cb = Environ.lookup_constant c env in 
+    let inst = Univ.AUContext.instance (Declareops.constant_polymorphic_context cb) in
+    let ty = Typeops.type_of_constant_type env cb.Declarations.const_type in
+    Vars.subst_instance_constr inst ty
   | IndRef ind ->
-     let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
-     let inst = Declareops.inductive_polymorphic_instance mib in
-       Inductive.type_of_inductive env (specif, inst)
+    let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
+    let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in
+    Inductive.type_of_inductive env (specif, inst)
   | ConstructRef cstr ->
-     let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
-     let inst = Declareops.inductive_polymorphic_instance mib in
-     Inductive.type_of_constructor (cstr,inst) specif
+    let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
+    let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in
+    Inductive.type_of_constructor (cstr,inst) specif
 
 let type_of_global_in_context env r = 
   match r with
   | VarRef id -> Environ.named_type id env, Univ.UContext.empty
   | ConstRef c -> 
-     let cb = Environ.lookup_constant c env in 
-     let univs =
-       Declareops.universes_of_polymorphic_constant
-         (Environ.opaque_tables env) cb in
-       Typeops.type_of_constant_type env cb.Declarations.const_type, univs
+    let cb = Environ.lookup_constant c env in 
+    let univs = Declareops.constant_polymorphic_context cb in
+    let inst = Univ.AUContext.instance univs in
+    let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
+    Typeops.type_of_constant_type env cb.Declarations.const_type, univs
   | IndRef ind ->
-     let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
-     let univs = Declareops.inductive_polymorphic_context mib in
-     Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs
+    let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    let inst = Univ.AUContext.instance univs in
+    let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
+    Inductive.type_of_inductive env (specif, inst), univs
   | ConstructRef cstr ->
     let (mib,oib as specif) =
       Inductive.lookup_mind_specif env (inductive_of_constructor cstr) 
     in
     let univs = Declareops.inductive_polymorphic_context mib in
-    let inst = Univ.UContext.instance univs in
+    let inst = Univ.AUContext.instance univs in
+    let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
     Inductive.type_of_constructor (cstr,inst) specif, univs
 
 let universes_of_global env r = 
     match r with
-    | VarRef id -> Univ.UContext.empty
+    | VarRef id -> Univ.AUContext.empty
     | ConstRef c -> 
       let cb = Environ.lookup_constant c env in 
-	Declareops.universes_of_polymorphic_constant
-          (Environ.opaque_tables env) cb
+      Declareops.constant_polymorphic_context cb
     | IndRef ind ->
       let (mib, oib) = Inductive.lookup_mind_specif env ind in
       Declareops.inductive_polymorphic_context mib
diff --git a/library/global.mli b/library/global.mli
index 754fa1516..5ddf54b4a 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -141,7 +141,7 @@ val type_of_global_unsafe : Globnames.global_reference -> Constr.types
     [Evarutil.new_global] and [Retyping.get_type_of]. *)
 
 (** Returns the universe context of the global reference (whatever its polymorphic status is). *)
-val universes_of_global : Globnames.global_reference -> Univ.universe_context
+val universes_of_global : Globnames.global_reference -> Univ.abstract_universe_context
 
 (** {6 Retroknowledge } *)
 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 1cb694da6..9fc2573ac 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -198,7 +198,8 @@ let warn_projection_no_head_constant =
 let compute_canonical_projections warn (con,ind) =
   let env = Global.env () in
   let ctx = Environ.constant_context env con in
-  let u = Univ.UContext.instance ctx in
+  let u = Univ.AUContext.instance ctx in
+  let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
   let v = (mkConstU (con,u)) in
   let ctx = Univ.ContextSet.of_context ctx in
   let c = Environ.constant_value_in env (con,u) in
@@ -298,7 +299,7 @@ let error_not_structure ref =
 let check_and_decompose_canonical_structure ref =
   let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in
   let env = Global.env () in
-  let u = Environ.constant_instance env sp in
+  let u = Univ.AUContext.instance (Environ.constant_context env sp) in
   let vc = match Environ.constant_opt_value_in env (sp, u) with
     | Some vc -> vc
     | None -> error_not_structure ref in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 201f79c39..bae831b63 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -117,10 +117,10 @@ let typeclass_univ_instance (cl,u') =
       match cl.cl_impl with
       | ConstRef c -> 
         let cb = Global.lookup_constant c in
-        Declareops.constant_polymorphic_instance cb
+        Univ.AUContext.instance (Declareops.constant_polymorphic_context cb)
       | IndRef c ->
          let mib,oib = Global.lookup_inductive c in
-         Declareops.inductive_polymorphic_instance mib
+         Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib)
       | _ -> Univ.Instance.empty
     in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) 
       Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u')
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index b3eaa3cb9..66cc42cb6 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -174,7 +174,7 @@ and nf_whd env sigma whd typ =
   | Vatom_stk(Aind ((mi,i) as ind), stk) ->
      let mib = Environ.lookup_mind mi env in
      let nb_univs =
-       Univ.Instance.length (Declareops.inductive_polymorphic_instance mib)
+       Univ.AUContext.size (Declareops.inductive_polymorphic_context mib)
      in
      let mk u =
        let pind = (ind, u) in (mkIndU pind, type_of_ind env pind)
@@ -203,7 +203,7 @@ and constr_type_of_idkey env sigma (idkey : Vars.id_key) stk =
   | ConstKey cst ->
      let cbody = Environ.lookup_constant cst env in
      let nb_univs =
-       Univ.Instance.length (Declareops.constant_polymorphic_instance cbody)
+       Univ.AUContext.size (Declareops.constant_polymorphic_context cbody)
      in
      let mk u =
        let pcst = (cst, u) in (mkConstU pcst, Typeops.type_of_constant_in env pcst)
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 15c0f80b9..d9bb97be1 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -78,6 +78,8 @@ let print_ref reduce ref =
       in EConstr.it_mkProd_or_LetIn ccl ctx
     else typ in
   let univs = Global.universes_of_global ref in
+  let inst = Univ.AUContext.instance univs in
+  let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
   let env = Global.env () in
   let bl = Universes.universe_binders_of_global ref in
   let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
@@ -503,7 +505,10 @@ let ungeneralized_type_of_constant_type t =
 
 let print_instance sigma cb =
   if Declareops.constant_is_polymorphic cb then
-    pr_universe_instance sigma (Declareops.constant_polymorphic_context cb)
+    let univs = Declareops.constant_polymorphic_context cb in
+    let inst = Univ.AUContext.instance univs in
+    let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
+    pr_universe_instance sigma univs
   else mt()
 				
 let print_constant with_values sep sp =
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 10b791e37..2e0e6d284 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -89,7 +89,7 @@ let build_ind_type env mip =
 
 let print_one_inductive env sigma mib ((_,i) as ind) =
   let u = if Declareops.inductive_is_polymorphic mib then 
-      Declareops.inductive_polymorphic_instance mib
+      Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib)
     else Univ.Instance.empty in
   let mip = mib.mind_packets.(i) in
   let params = Inductive.inductive_paramdecls (mib,u) in
@@ -100,7 +100,9 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
   let envpar = push_rel_context params env in
   let inst =
     if Declareops.inductive_is_polymorphic mib then
-      Printer.pr_universe_instance sigma (Declareops.inductive_polymorphic_context mib)
+      let ctx = Declareops.inductive_polymorphic_context mib in
+      let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
+      Printer.pr_universe_instance sigma ctx
     else mt ()
   in
   hov 0 (
@@ -149,7 +151,7 @@ let get_fields =
 let print_record env mind mib =
   let u = 
     if Declareops.inductive_is_polymorphic mib then 
-      Declareops.inductive_polymorphic_instance mib
+      Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib)
     else Univ.Instance.empty 
   in
   let mip = mib.mind_packets.(0) in
@@ -292,11 +294,13 @@ let print_body is_impl env mp (l,body) =
     | SFBmodule _ -> keyword "Module" ++ spc () ++ name
     | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name
     | SFBconst cb ->
+       let ctx = Declareops.constant_polymorphic_context cb in
        let u =
 	 if Declareops.constant_is_polymorphic cb then
-            Declareops.constant_polymorphic_instance cb
+            Univ.AUContext.instance ctx
 	 else Univ.Instance.empty
        in
+       let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
        let sigma = Evd.empty in
       (match cb.const_body with
 	| Def _ -> def "Definition" ++ spc ()
@@ -316,8 +320,7 @@ let print_body is_impl env mp (l,body) =
 		       Printer.pr_lconstr_env env sigma
 			  (Vars.subst_instance_constr u (Mod_subst.force_constr l)))
 	      | _ -> mt ()) ++ str "." ++
-	    Printer.pr_universe_ctx sigma 
-              (Declareops.constant_polymorphic_context cb))
+	    Printer.pr_universe_ctx sigma ctx)
     | SFBmind mib ->
       try
 	let env = Option.get env in
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 5d9d36958..e058806a3 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -48,7 +48,8 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
   else
     let mib,mip = Inductive.lookup_mind_specif env ind in
     let ctx = Declareops.inductive_polymorphic_context mib in
-    let u = Univ.UContext.instance ctx in
+    let u = Univ.AUContext.instance ctx in
+    let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
     let ctxset = Univ.ContextSet.of_context ctx in
     let ectx = Evd.evar_universe_context_of ctxset in
     let sigma = Evd.merge_universe_context sigma ectx in
@@ -62,7 +63,8 @@ let build_induction_scheme_in_type dep sort ind =
     let mib,mip = Inductive.lookup_mind_specif env ind in
       Declareops.inductive_polymorphic_context mib
   in
-  let u = Univ.UContext.instance ctx in
+  let u = Univ.AUContext.instance ctx in
+  let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
   let ctxset = Univ.ContextSet.of_context ctx in
   let sigma = Evd.merge_universe_context sigma (Evd.evar_universe_context_of ctxset) in
   let sigma, c = build_induction_scheme env sigma (ind,u) dep sort in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index c0acdaf57..5a1c260b1 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -362,7 +362,7 @@ let get_body obl =
   match obl.obl_body with
   | None -> None
   | Some (DefinedObl c) ->
-    let u = Environ.constant_instance (Global.env ()) c in
+    let u = Univ.AUContext.instance (Environ.constant_context (Global.env ()) c) in
     let pc = (c, u) in
       Some (DefinedObl pc)
   | Some (TermObl c) ->
diff --git a/vernac/record.ml b/vernac/record.ml
index d61f44cac..366f50454 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -265,7 +265,7 @@ let warn_non_primitive_record =
 let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
-  let u = Declareops.inductive_polymorphic_instance mib in
+  let u = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in
   let paramdecls = Inductive.inductive_paramdecls (mib, u) in
   let poly = Declareops.inductive_is_polymorphic mib in
   let ctx =
@@ -547,7 +547,7 @@ let add_inductive_class ind =
   let mind, oneind = Global.lookup_inductive ind in
   let k =
     let ctx = oneind.mind_arity_ctxt in
-    let inst = Declareops.inductive_polymorphic_instance mind in
+    let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mind) in
     let ty = Inductive.type_of_inductive
       (push_rel_context ctx (Global.env ()))
       ((mind,oneind),inst)
diff --git a/vernac/search.ml b/vernac/search.ml
index 00536e52e..788a2aa4a 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -85,7 +85,7 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) =
     let mib = Global.lookup_mind mind in
     let iter_packet i mip =
       let ind = (mind, i) in
-      let u = Declareops.inductive_polymorphic_instance mib in
+      let u = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in
       let i = (ind, u) in
       let typ = Inductiveops.type_of_inductive env i in
       let () = fn (IndRef ind) env typ in