Merge PR #11731: [proof] Miscellaneous refactorings

Reviewed-by: SkySkimmer
Reviewed-by: gares

7 files changed, 33 insertions, 36 deletions

diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 9b0a323078..e85d94cd72 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 ~sign: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 438892e75e..b228a04298 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -116,31 +116,31 @@ 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 sigma ~poly typ tac =
+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 sigma 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, status, univs
+  cb, ce.Declare.proof_entry_type, status, univs
 
 let refine_by_tactic ~name ~poly env sigma ty tac =
   (* Save the initial side-effects to restore them afterwards. We set the
diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli
index 3cf3a13262..c49e997757 100644
--- a/tactics/pfedit.mli
+++ b/tactics/pfedit.mli
@@ -64,8 +64,8 @@ val use_unification_heuristics : unit -> bool
 val build_constant_by_tactic
   :  name:Id.t
   -> ?opaque:Proof_global.opacity_flag
-  -> UState.t
-  -> named_context_val
+  -> uctx:UState.t
+  -> sign:named_context_val
   -> poly:bool
   -> EConstr.types
   -> unit Proofview.tactic
@@ -74,11 +74,11 @@ val build_constant_by_tactic
 val build_by_tactic
   :  ?side_eff:bool
   -> env
-  -> UState.t
+  -> uctx:UState.t
   -> poly:bool
-  -> EConstr.types
+  -> typ:EConstr.types
   -> unit Proofview.tactic
-  -> constr * bool * UState.t
+  -> constr * types option * bool * UState.t
 
 val refine_by_tactic
   :  name:Id.t
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index 7d59a18494..7fd1634dcf 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -27,8 +27,7 @@ module NamedDecl = Context.Named.Declaration
 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 +158,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 +166,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 +181,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 +191,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 +206,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 +214,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 +239,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; 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..f1281d1291 100644
--- a/tactics/proof_global.mli
+++ b/tactics/proof_global.mli
@@ -33,9 +33,7 @@ type proof_object =
   (** name of the proof *)
   ; entries : Evd.side_effects Declare.proof_entry list
   (** 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 *)