Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layers

13 files changed, 80 insertions, 80 deletions

diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index db07bbd068..86bbf46a35 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -187,7 +187,7 @@ let rec traverse current ctx accu t = match kind_of_term t with
   let body () = id |> Global.lookup_named |> NamedDecl.get_value in
   traverse_object accu body (VarRef id)
 | Const (kn, _) ->
-  let body () = Global.body_of_constant_body (lookup_constant kn) in
+  let body () = Option.map fst (Global.body_of_constant_body (lookup_constant kn)) in
   traverse_object accu body (ConstRef kn)
 | Ind ((mind, _) as ind, _) ->
   traverse_inductive accu mind (IndRef ind)
@@ -200,7 +200,7 @@ let rec traverse current ctx accu t = match kind_of_term t with
     | Lambda(_,_,oty), Const (kn, _)
       when Vars.noccurn 1 oty &&
       not (Declareops.constant_has_body (lookup_constant kn)) ->
-        let body () = Global.body_of_constant_body (lookup_constant kn) in
+        let body () = Option.map fst (Global.body_of_constant_body (lookup_constant kn)) in
         traverse_object
           ~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn)
     | _ ->
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 248224e6b7..59920742d8 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -105,7 +105,7 @@ let mkFullInd (ind,u) n =
     else mkIndU (ind,u)
 
 let check_bool_is_defined () =
-  try let _ = Global.type_of_global_unsafe Coqlib.glob_bool in ()
+  try let _ = Global.type_of_global_in_context (Global.env ()) Coqlib.glob_bool in ()
   with e when CErrors.noncritical e -> raise (UndefinedCst "bool")
 
 let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
diff --git a/vernac/class.ml b/vernac/class.ml
index 0b510bbcf0..be682977e5 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -62,7 +62,9 @@ let explain_coercion_error g = function
 (* Verifications pour l'ajout d'une classe *)
 
 let check_reference_arity ref =
-  if not (Reductionops.is_arity (Global.env()) Evd.empty (EConstr.of_constr (Global.type_of_global_unsafe ref))) (** FIXME *) then
+  let env = Global.env () in
+  let c, _ = Global.type_of_global_in_context env ref in
+  if not (Reductionops.is_arity env Evd.empty (EConstr.of_constr c)) (** FIXME *) then
     raise (CoercionError (NotAClass ref))
 
 let check_arity = function
@@ -252,7 +254,7 @@ let warn_uniform_inheritance =
 
 let add_new_coercion_core coef stre poly source target isid =
   check_source source;
-  let t = Global.type_of_global_unsafe coef in
+  let t, _ = Global.type_of_global_in_context (Global.env ()) coef in
   if coercion_exists coef then raise (CoercionError AlreadyExists);
   let tg,lp = prods_of t in
   let llp = List.length lp in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index a528b96407..ab1892a18e 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -68,7 +68,7 @@ let _ =
 let existing_instance glob g info =
   let c = global g in
   let info = Option.default Hints.empty_hint_info info in
-  let instance = Global.type_of_global_unsafe c in
+  let instance, _ = Global.type_of_global_in_context (Global.env ()) c in
   let _, r = decompose_prod_assum instance in
     match class_of_constr Evd.empty (EConstr.of_constr r) with
       | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob
@@ -164,7 +164,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
     let ctx'' = ctx' @ ctx in
     let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) !evars (EConstr.of_constr c) in
     let u = EConstr.EInstance.kind !evars u in
-    let cl, u = Typeclasses.typeclass_univ_instance (k, u) in
+    let cl = Typeclasses.typeclass_univ_instance (k, u) in
     let _, args = 
       List.fold_right (fun decl (args, args') ->
 	match decl with
diff --git a/vernac/discharge.ml b/vernac/discharge.ml
index b6308aba00..474c0b4dd2 100644
--- a/vernac/discharge.ml
+++ b/vernac/discharge.ml
@@ -77,42 +77,36 @@ let refresh_polymorphic_type_of_inductive (_,mip) =
     let ctx = List.rev mip.mind_arity_ctxt in
       mkArity (List.rev ctx, Type ar.template_level), true
 
-let process_inductive (sechyps,abs_ctx) modlist mib =
+let process_inductive (sechyps,_,_ as info) modlist mib =
+  let sechyps = Lib.named_of_variable_context sechyps in
   let nparams = mib.mind_nparams in
-  let subst, univs =
+  let subst, ind_univs =
     match mib.mind_universes with
-    | Monomorphic_ind ctx -> Univ.Instance.empty, ctx
+    | Monomorphic_ind ctx -> Univ.empty_level_subst, Monomorphic_ind_entry ctx
     | Polymorphic_ind auctx ->
-      Univ.AUContext.instance auctx, Univ.instantiate_univ_context auctx
+      let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
+      let auctx = Univ.AUContext.repr auctx in
+      subst, Polymorphic_ind_entry auctx
     | Cumulative_ind cumi ->
       let auctx = Univ.ACumulativityInfo.univ_context cumi in
-      Univ.AUContext.instance auctx, Univ.instantiate_univ_context auctx
+      let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
+      let auctx = Univ.AUContext.repr auctx in
+      subst, Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context auctx)
   in
+  let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in
   let inds =
     Array.map_to_list
       (fun mip ->
 	let ty, template = refresh_polymorphic_type_of_inductive (mib,mip) in
-	let arity = expmod_constr modlist ty in
-	let arity = Vars.subst_instance_constr subst arity in
-	let lc = Array.map 
-	  (fun c -> Vars.subst_instance_constr subst (expmod_constr modlist c))
-	  mip.mind_user_lc 
-	in
+        let arity = discharge ty in
+        let lc = Array.map discharge mip.mind_user_lc  in
 	  (mip.mind_typename,
 	   arity, template,
 	   Array.to_list mip.mind_consnames,
 	   Array.to_list lc))
       mib.mind_packets in
-  let sechyps' = Context.Named.map (expmod_constr modlist) sechyps in
+  let sechyps' = Context.Named.map discharge sechyps in
   let (params',inds') = abstract_inductive sechyps' nparams inds in
-  let abs_ctx = Univ.instantiate_univ_context abs_ctx in
-  let univs = Univ.UContext.union abs_ctx univs in
-  let ind_univs =
-    match mib.mind_universes with
-    | Monomorphic_ind _ -> Monomorphic_ind_entry univs
-    | Polymorphic_ind _ -> Polymorphic_ind_entry univs
-    | Cumulative_ind _ ->
-      Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs) in
   let record = match mib.mind_record with
     | Some (Some (id, _, _)) -> Some (Some id)
     | Some None -> Some None
diff --git a/vernac/discharge.mli b/vernac/discharge.mli
index a0dabe2f46..c8c7e3b8b8 100644
--- a/vernac/discharge.mli
+++ b/vernac/discharge.mli
@@ -11,5 +11,4 @@ open Entries
 open Opaqueproof
 
 val process_inductive :
-  ((Term.constr, Term.constr) Context.Named.pt * Univ.abstract_universe_context)
-  -> work_list -> mutual_inductive_body -> mutual_inductive_entry
+  Lib.abstr_info -> work_list -> mutual_inductive_body -> mutual_inductive_entry
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 86dcb6d4dc..784c6d3387 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -909,7 +909,7 @@ let explain_not_match_error = function
       quote (Printer.safe_pr_lconstr_env env Evd.empty t2)
   | IncompatibleConstraints cst ->
     str " the expected (polymorphic) constraints do not imply " ++
-      let cst = Univ.UContext.constraints (Univ.instantiate_univ_context cst) in
+      let cst = Univ.AUContext.instantiate (Univ.AUContext.instance cst) cst in
       quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst)
 
 let explain_signature_mismatch l spec why =
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 6d93f0e410..3d97a767c8 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -383,9 +383,8 @@ let do_mutual_induction_scheme lnamedepindsort =
 	 match inst with
 	 | None ->
 	    let _, ctx = Global.type_of_global_in_context env0 (IndRef ind) in
-	    let ctxs = Univ.ContextSet.of_context ctx in
-	    let evd = Evd.from_ctx (Evd.evar_universe_context_of ctxs) in
-	    let u = Univ.UContext.instance ctx in
+	    let u, ctx = Universes.fresh_instance_from ctx None in
+	    let evd = Evd.from_ctx (Evd.evar_universe_context_of ctx) in
 	      evd, (ind,u), Some u
 	 | Some ui -> evd, (ind, ui), inst
        in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 2eeaf4d5dc..645320c603 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -44,12 +44,15 @@ let call_hook fix_exn hook l c =
 
 (* Support for mutually proved theorems *)
 
-let retrieve_first_recthm = function
+let retrieve_first_recthm uctx = function
   | VarRef id ->
       (NamedDecl.get_value (Global.lookup_named id),variable_opacity id)
   | ConstRef cst ->
       let cb = Global.lookup_constant cst in
-      (Global.body_of_constant_body cb, is_opaque cb)
+      let (_, uctx) = UState.universe_context uctx in
+      let inst = Univ.UContext.instance uctx in
+      let map (c, ctx) = Vars.subst_instance_constr inst c in
+      (Option.map map (Global.body_of_constant_body cb), is_opaque cb)
   | _ -> assert false
 
 let adjust_guardness_conditions const = function
@@ -412,7 +415,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
         let other_thms_data =
           if List.is_empty other_thms then [] else
             (* there are several theorems defined mutually *)
-            let body,opaq = retrieve_first_recthm ref in
+            let body,opaq = retrieve_first_recthm ctx ref in
             let subst = Evd.evar_universe_context_subst ctx in
             let norm c = Universes.subst_opt_univs_constr subst c in
 	    let ctx = UState.context_set (*FIXME*) ctx in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 5a1c260b1f..4b1565d3ce 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -285,7 +285,7 @@ type obligation =
   { obl_name : Id.t;
     obl_type : types;
     obl_location : Evar_kinds.t Loc.located;
-    obl_body : constant obligation_body option;
+    obl_body : pconstant obligation_body option;
     obl_status : bool * Evar_kinds.obligation_definition_status;
     obl_deps : Int.Set.t;
     obl_tac : unit Proofview.tactic option;
@@ -358,18 +358,8 @@ let _ =
 
 let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type
 
-let get_body obl =
-  match obl.obl_body with
-  | None -> None
-  | Some (DefinedObl c) ->
-    let u = Univ.AUContext.instance (Environ.constant_context (Global.env ()) c) in
-    let pc = (c, u) in
-      Some (DefinedObl pc)
-  | Some (TermObl c) ->
-      Some (TermObl c)
-
 let get_obligation_body expand obl =
-  match get_body obl with
+  match obl.obl_body with
   | None -> None
   | Some c ->
      if expand && snd obl.obl_status == Evar_kinds.Expand then
@@ -664,7 +654,7 @@ let declare_obligation prg obl body ty uctx =
 	definition_message obl.obl_name;
 	true, { obl with obl_body =
 	    if poly then
-	      Some (DefinedObl constant)
+	      Some (DefinedObl (constant, Univ.UContext.instance uctx))
 	    else
 	      Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) }
 
@@ -892,20 +882,22 @@ let obligation_hook prg obl num auto ctx' _ gr =
        if not transparent then err_not_transp ()
     | _ -> ()
 in
-  let obl = { obl with obl_body = Some (DefinedObl cst) } in
-  let () = if transparent then add_hint true prg cst in
-  let obls = Array.copy obls in
-  let _ = obls.(num) <- obl in
   let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in
-  let ctx' =
+  let inst, ctx' =
     if not (pi2 prg.prg_kind) (* Not polymorphic *) then
       (* The universe context was declared globally, we continue
          from the new global environment. *)
       let evd = Evd.from_env (Global.env ()) in
       let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in
-        Evd.evar_universe_context ctx'
-    else ctx'
+      Univ.Instance.empty, Evd.evar_universe_context ctx'
+    else
+      let (_, uctx) = UState.universe_context ctx' in
+      Univ.UContext.instance uctx, ctx'
   in
+  let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in
+  let () = if transparent then add_hint true prg cst in
+  let obls = Array.copy obls in
+  let _ = obls.(num) <- obl in
   let prg = { prg with prg_ctx = ctx' } in
   let () =
     try ignore (update_obls prg obls (pred rem))
@@ -1132,7 +1124,7 @@ let admit_prog prg =
               (ParameterEntry (None,false,(x.obl_type,ctx),None), IsAssumption Conjectural)
             in
               assumption_message x.obl_name;
-              obls.(i) <- { x with obl_body = Some (DefinedObl kn) }
+              obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) }
         | Some _ -> ())
       obls;
     ignore(update_obls prg obls 0)
diff --git a/vernac/record.ml b/vernac/record.ml
index 366f504545..63ca227862 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -265,16 +265,10 @@ 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 = 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 =
-    match mib.mind_universes with
-    | Monomorphic_ind ctx -> ctx
-    | Polymorphic_ind auctx -> Univ.instantiate_univ_context auctx
-    | Cumulative_ind cumi -> 
-      Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi)
-  in
+  let ctx = Univ.AUContext.repr (Declareops.inductive_polymorphic_context mib) in
+  let u = Univ.UContext.instance ctx in
+  let paramdecls = Inductive.inductive_paramdecls (mib, u) in
   let indu = indsp, u in
   let r = mkIndU (indsp,u) in
   let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in
@@ -334,8 +328,7 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
 		    const_entry_secctx = None;
 		    const_entry_type = Some projtyp;
 		    const_entry_polymorphic = poly;
-		    const_entry_universes =
-		      if poly then ctx else Univ.UContext.empty;
+		    const_entry_universes = ctx;
 		    const_entry_opaque = false;
 		    const_entry_inline_code = false;
 		    const_entry_feedback = None } in
@@ -431,6 +424,12 @@ let declare_structure finite univs id idbuild paramimpls params arity template
   let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
   let cstr = (rsp,1) in
+  let fields =
+    if poly then
+      let subst, _ = Univ.abstract_universes ctx in
+      Context.Rel.map (fun c -> Vars.subst_univs_level_constr subst c) fields
+    else fields
+  in
   let kinds,sp_projs = declare_projections rsp ~kind binder_name coers fieldimpls fields in
   let build = ConstructRef cstr in
   let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
@@ -518,8 +517,18 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity
       | None -> None)
       params, params
   in
+  let univs, ctx_context, fields =
+    if poly then
+      let usubst, auctx = Univ.abstract_universes ctx in
+      let map c = Vars.subst_univs_level_constr usubst c in
+      let fields = Context.Rel.map map fields in
+      let ctx_context = on_snd (fun d -> Context.Rel.map map d) ctx_context in
+      auctx, ctx_context, fields
+    else Univ.AUContext.empty, ctx_context, fields
+  in
   let k =
-    { cl_impl = impl;
+    { cl_univs = univs;
+      cl_impl = impl;
       cl_strict = !typeclasses_strict;
       cl_unique = !typeclasses_unique;
       cl_context = ctx_context;
@@ -530,10 +539,11 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity
 
 
 let add_constant_class cst =
-  let ty = Universes.unsafe_type_of_global (ConstRef cst) in
+  let ty, univs = Global.type_of_global_in_context (Global.env ()) (ConstRef cst) in
   let ctx, arity = decompose_prod_assum ty in
   let tc = 
-    { cl_impl = ConstRef cst;
+    { cl_univs = univs;
+      cl_impl = ConstRef cst;
       cl_context = (List.map (const None) ctx, ctx);
       cl_props = [LocalAssum (Anonymous, arity)];
       cl_projs = [];
@@ -547,12 +557,13 @@ let add_inductive_class ind =
   let mind, oneind = Global.lookup_inductive ind in
   let k =
     let ctx = oneind.mind_arity_ctxt 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)
-    in
-      { cl_impl = IndRef ind;
+    let univs = Declareops.inductive_polymorphic_context mind in
+    let env = push_context ~strict:false (Univ.AUContext.repr univs) (Global.env ()) in
+    let env = push_rel_context ctx env in
+    let inst = Univ.make_abstract_instance univs in
+    let ty = Inductive.type_of_inductive env ((mind, oneind), inst) in
+      { cl_univs = univs;
+        cl_impl = IndRef ind;
 	cl_context = List.map (const None) ctx, ctx;
 	cl_props = [LocalAssum (Anonymous, ty)];
 	cl_projs = [];
diff --git a/vernac/search.ml b/vernac/search.ml
index 788a2aa4a9..0f56f81e74 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -78,14 +78,14 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) =
   | "CONSTANT" ->
     let cst = Global.constant_of_delta_kn kn in
     let gr = ConstRef cst in
-    let typ = Global.type_of_global_unsafe gr in
+    let (typ, _) = Global.type_of_global_in_context (Global.env ()) gr in
       fn gr env typ
   | "INDUCTIVE" ->
     let mind = Global.mind_of_delta_kn kn in
     let mib = Global.lookup_mind mind in
     let iter_packet i mip =
       let ind = (mind, i) in
-      let u = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in
+      let u = Univ.make_abstract_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
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index bbec28afff..8a647c6c18 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -986,7 +986,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
 
   let sr = smart_global reference in
   let inf_names =
-    let ty = Global.type_of_global_unsafe sr in
+    let ty, _ = Global.type_of_global_in_context (Global.env ()) sr in
     Impargs.compute_implicits_names (Global.env ()) ty
   in
   let prev_names =