[declare] Remaining bits on the consistency of UState.t naming

10 files changed, 39 insertions, 39 deletions

diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 9b0a323078..9aa5170a29 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -91,7 +91,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in
   let ectx = Evd.evar_universe_context sigma in
   let (const, safe, ectx) =
-    try Pfedit.build_constant_by_tactic ~name ~opaque:Proof_global.Transparent ~poly ectx secsign concl solve_tac
+    try Pfedit.build_constant_by_tactic ~name ~opaque:Proof_global.Transparent ~poly ~uctx:ectx secsign concl solve_tac
     with Logic_monad.TacticFailure e as src ->
     (* if the tactic [tac] fails, it reports a [TacticFailure e],
        which is an error irrelevant to the proof system (in fact it
diff --git a/tactics/declare.ml b/tactics/declare.ml
index de3c731d9b..5e6f78be6f 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -351,11 +351,11 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind
   let eff = { Evd.seff_private = eff; Evd.seff_roles; } in
   kn, eff
 
-let inline_private_constants ~univs env ce =
+let inline_private_constants ~uctx env ce =
   let body, eff = Future.force ce.proof_entry_body in
   let cb, ctx = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in
-  let univs = UState.merge ~sideff:true Evd.univ_rigid univs ctx in
-  cb, univs
+  let uctx = UState.merge ~sideff:true Evd.univ_rigid uctx ctx in
+  cb, uctx
 
 (** Declaration of section variables and local definitions *)
 type variable_declaration =
@@ -382,13 +382,13 @@ let declare_variable ~name ~kind d =
     | SectionLocalDef (de) ->
       (* The body should already have been forced upstream because it is a
          section-local definition, but it's not enforced by typing *)
-      let ((body, uctx), eff) = Future.force de.proof_entry_body in
+      let ((body, body_ui), eff) = Future.force de.proof_entry_body in
       let () = export_side_effects eff in
-      let poly, univs = match de.proof_entry_universes with
+      let poly, entry_ui = match de.proof_entry_universes with
         | Monomorphic_entry uctx -> false, uctx
         | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
       in
-      let univs = Univ.ContextSet.union uctx univs in
+      let univs = Univ.ContextSet.union body_ui entry_ui in
       (* We must declare the universe constraints before type-checking the
          term. *)
       let () = declare_universe_context ~poly univs in
diff --git a/tactics/declare.mli b/tactics/declare.mli
index f87d08fc8b..0068b9842a 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -108,11 +108,11 @@ val declare_private_constant
   -> unit proof_entry
   -> Constant.t * Evd.side_effects
 
-(** [inline_private_constants ~sideff ~univs env ce] will inline the
+(** [inline_private_constants ~sideff ~uctx env ce] will inline the
    constants in [ce]'s body and return the body plus the updated
    [UState.t]. *)
 val inline_private_constants
-  :  univs:UState.t
+  :  uctx:UState.t
   -> Environ.env
   -> Evd.side_effects proof_entry
   -> Constr.t * UState.t
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
index a2edb5fe49..c02b198bf7 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -116,29 +116,29 @@ let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None t
 
 let next = let n = ref 0 in fun () -> incr n; !n
 
-let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ctx sign ~poly typ tac =
-  let evd = Evd.from_ctx ctx in
+let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ~uctx sign ~poly typ tac =
+  let evd = Evd.from_ctx uctx in
   let goals = [ (Global.env_of_context sign , typ) ] in
   let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in
   let pf, status = by tac pf in
   let open Proof_global in
-  let { entries; universes } = close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pf in
+  let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pf in
   match entries with
   | [entry] ->
-    entry, status, universes
+    entry, status, uctx
   | _ ->
     CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term")
 
 let build_by_tactic ?(side_eff=true) env ~uctx ~poly ~typ tac =
   let name = Id.of_string ("temporary_proof"^string_of_int (next())) in
   let sign = val_of_named_context (named_context env) in
-  let ce, status, univs = build_constant_by_tactic ~name uctx sign ~poly typ tac in
-  let cb, univs =
-    if side_eff then Declare.inline_private_constants ~univs env ce
+  let ce, status, univs = build_constant_by_tactic ~name ~uctx sign ~poly typ tac in
+  let cb, uctx =
+    if side_eff then Declare.inline_private_constants ~uctx env ce
     else
       (* GG: side effects won't get reset: no need to treat their universes specially *)
       let (cb, ctx), _eff = Future.force ce.Declare.proof_entry_body in
-      cb, UState.merge ~sideff:false Evd.univ_rigid univs ctx
+      cb, UState.merge ~sideff:false Evd.univ_rigid uctx ctx
   in
   cb, ce.Declare.proof_entry_type, status, univs
 
diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli
index c1f656376d..8085153df0 100644
--- a/tactics/pfedit.mli
+++ b/tactics/pfedit.mli
@@ -64,7 +64,7 @@ val use_unification_heuristics : unit -> bool
 val build_constant_by_tactic
   :  name:Id.t
   -> ?opaque:Proof_global.opacity_flag
-  -> UState.t
+  -> uctx:UState.t
   -> named_context_val
   -> poly:bool
   -> EConstr.types
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index 7d59a18494..ca3a90ccbd 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -28,7 +28,7 @@ type proof_object =
   { name : Names.Id.t
   ; entries : Evd.side_effects Declare.proof_entry list
   ; poly : bool
-  ; universes: UState.t
+  ; uctx: UState.t
   ; udecl : UState.universe_decl
   }
 
@@ -159,7 +159,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
     UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx
   in
   let fpl, univs = Future.split2 fpl in
-  let universes = if poly || now then Future.force univs else initial_euctx in
+  let uctx = if poly || now then Future.force univs else initial_euctx in
   (* Because of dependent subgoals at the beginning of proofs, we could
      have existential variables in the initial types of goals, we need to
      normalise them for the kernel. *)
@@ -167,7 +167,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
     let { Proof.sigma } = Proof.data proof in
     Evd.existential_opt_value0 sigma k in
   let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar
-    (UState.subst universes) in
+    (UState.subst uctx) in
 
   let make_body =
     if poly || now then
@@ -182,7 +182,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
         let used_univs_typ = Vars.universes_of_constr typ in
         if allow_deferred then
           let initunivs = UState.univ_entry ~poly initial_euctx in
-          let ctx = constrain_variables universes in
+          let ctx = constrain_variables uctx in
           (* For vi2vo compilation proofs are computed now but we need to
              complement the univ constraints of the typ with the ones of
              the body.  So we keep the two sets distinct. *)
@@ -192,7 +192,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
           (initunivs, typ), ((body, univs), eff)
         else if poly && opaque && private_poly_univs () then
           let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-          let universes = UState.restrict universes used_univs in
+          let universes = UState.restrict uctx used_univs in
           let typus = UState.restrict universes used_univs_typ in
           let udecl = UState.check_univ_decl ~poly typus udecl in
           let ubody = Univ.ContextSet.diff
@@ -207,7 +207,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
              the actually used universes.
              TODO: check if restrict is really necessary now. *)
           let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-          let ctx = UState.restrict universes used_univs in
+          let ctx = UState.restrict uctx used_univs in
           let univs = UState.check_univ_decl ~poly ctx udecl in
           (univs, typ), ((body, Univ.ContextSet.empty), eff)
       in
@@ -215,7 +215,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
     else
       fun t p ->
         (* Already checked the univ_decl for the type universes when starting the proof. *)
-        let univctx = UState.univ_entry ~poly:false universes in
+        let univctx = UState.univ_entry ~poly:false uctx in
         let t = nf t in
         Future.from_val (univctx, t),
         Future.chain p (fun (pt,eff) ->
@@ -240,7 +240,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
     Declare.delayed_definition_entry ~opaque ?feedback_id ?section_vars ~univs ~types:typ body
   in
   let entries = Future.map2 entry_fn fpl (Proofview.initial_goals entry) in
-  { name; entries; poly; universes; udecl }
+  { name; entries; poly; uctx; udecl }
 
 let return_proof ?(allow_partial=false) ps =
  let { proof } = ps in
diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli
index 8c1bc0def1..7b806f878d 100644
--- a/tactics/proof_global.mli
+++ b/tactics/proof_global.mli
@@ -35,7 +35,7 @@ type proof_object =
   (** list of the proof terms (in a form suitable for definitions). *)
   ; poly : bool
   (** polymorphic status *)
-  ; universes: UState.t
+  ; uctx: UState.t
   (** universe state *)
   ; udecl : UState.universe_decl
   (** universe declaration *)
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index a0be092e7e..8b0666aab7 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -489,7 +489,7 @@ let obligation_terminator entries uctx { name; num; auto } =
   | [entry] ->
     let env = Global.env () in
     let ty = entry.Declare.proof_entry_type in
-    let body, uctx = Declare.inline_private_constants ~univs:uctx env entry in
+    let body, uctx = Declare.inline_private_constants ~uctx env entry in
     let sigma = Evd.from_ctx uctx in
     Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body);
     (* Declare the obligation ourselves and drop the hook *)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 3646e73ce1..e5d9847c4a 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -356,17 +356,17 @@ let finish_proved idopt po info =
   let open Proof_global in
   let { Info.hook } = info in
   match po with
-  | { name; entries=[const]; universes; udecl; poly } ->
+  | { name; entries=[const]; uctx; udecl; poly } ->
     let name = match idopt with
       | None -> name
       | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in
     let fix_exn = Declare.Internal.get_fix_exn const in
     let () = try
       let mutpe = MutualEntry.adjust_guardness_conditions ~info const in
-      let hook_data = Option.map (fun hook -> hook, universes, []) hook in
-      let ubind = UState.universe_binders universes in
+      let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
+      let ubind = UState.universe_binders uctx in
       let _r : Names.GlobRef.t list =
-        MutualEntry.declare_mutdef ~fix_exn ~uctx:universes ~poly ~udecl ?hook_data ~ubind ~name mutpe
+        MutualEntry.declare_mutdef ~fix_exn ~uctx ~poly ~udecl ?hook_data ~ubind ~name mutpe
       in ()
     with e when CErrors.noncritical e ->
       let e = Exninfo.capture e in
@@ -439,7 +439,7 @@ let finalize_proof idopt proof_obj proof_info =
   | Regular ->
     finish_proved idopt proof_obj proof_info
   | End_obligation oinfo ->
-    DeclareObl.obligation_terminator proof_obj.entries proof_obj.universes oinfo
+    DeclareObl.obligation_terminator proof_obj.entries proof_obj.uctx oinfo
   | End_derive { f ; name } ->
     finish_derived ~f ~name ~idopt ~entries:proof_obj.entries
   | End_equations { hook; i; types; wits; sigma } ->
@@ -455,7 +455,7 @@ let save_lemma_proved ~lemma ~opaque ~idopt =
 (***********************************************************************)
 let save_lemma_admitted_delayed ~proof ~info =
   let open Proof_global in
-  let { name; entries; universes; udecl; poly } = proof in
+  let { name; entries; uctx; udecl; poly } = proof in
   if List.length entries <> 1 then
     CErrors.user_err Pp.(str "Admitted does not support multiple statements");
   let { Declare.proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
@@ -465,8 +465,8 @@ let save_lemma_admitted_delayed ~proof ~info =
   let typ = match proof_entry_type with
     | None -> CErrors.user_err Pp.(str "Admitted requires an explicit statement");
     | Some typ -> typ in
-  let ctx = UState.univ_entry ~poly universes in
+  let ctx = UState.univ_entry ~poly uctx in
   let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in
-  finish_admitted ~name ~poly ~uctx:universes ~udecl ~info (sec_vars, (typ, ctx), None)
+  finish_admitted ~name ~poly ~uctx ~udecl ~info (sec_vars, (typ, ctx), None)
 
 let save_lemma_proved_delayed ~proof ~info ~idopt = finalize_proof idopt proof info
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index c022d93f34..9418231cf5 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -420,10 +420,10 @@ let solve_by_tac ?loc name evi t poly uctx =
   try
     (* the status is dropped. *)
     let env = Global.env () in
-    let body, types, _, ctx' =
+    let body, types, _, uctx =
       Pfedit.build_by_tactic env ~uctx ~poly ~typ:evi.evar_concl t in
-    Inductiveops.control_only_guard env (Evd.from_ctx ctx') (EConstr.of_constr body);
-    Some (body, types, ctx')
+    Inductiveops.control_only_guard env (Evd.from_ctx uctx) (EConstr.of_constr body);
+    Some (body, types, uctx)
   with
   | Refiner.FailError (_, s) as exn ->
     let _ = Exninfo.capture exn in