[proof] finalize_proof doesn't need opaque (it's already in entries)

5 files changed, 25 insertions, 33 deletions

diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 81cde786c2..759e907bc9 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -497,7 +497,7 @@ type obligation_qed_info =
   ; auto : Id.t option -> Int.Set.t -> unit Proofview.tactic option -> progress
   }
 
-let obligation_terminator opq entries uctx { name; num; auto } =
+let obligation_terminator entries uctx { name; num; auto } =
   let open Proof_global in
   match entries with
   | [entry] ->
@@ -517,13 +517,13 @@ let obligation_terminator opq entries uctx { name; num; auto } =
     let obls, rem = prg.prg_obligations in
     let obl = obls.(num) in
     let status =
-      match obl.obl_status, opq with
-      | (_, Evar_kinds.Expand), Opaque -> err_not_transp ()
-      | (true, _), Opaque -> err_not_transp ()
-      | (false, _), Opaque -> Evar_kinds.Define true
-      | (_, Evar_kinds.Define true), Transparent ->
+      match obl.obl_status, entry.proof_entry_opaque with
+      | (_, Evar_kinds.Expand), true -> err_not_transp ()
+      | (true, _), true -> err_not_transp ()
+      | (false, _), true -> Evar_kinds.Define true
+      | (_, Evar_kinds.Define true), false ->
         Evar_kinds.Define false
-      | (_, status), Transparent -> status
+      | (_, status), false -> status
     in
     let obl = { obl with obl_status = false, status } in
     let ctx =
diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli
index 2d275b5ed8..fae27e1cb3 100644
--- a/vernac/declareObl.mli
+++ b/vernac/declareObl.mli
@@ -79,8 +79,7 @@ type obligation_qed_info =
   }
 
 val obligation_terminator
-  :  Proof_global.opacity_flag
-  -> Evd.side_effects Proof_global.proof_entry list
+  : Evd.side_effects Proof_global.proof_entry list
   -> UState.t
   -> obligation_qed_info -> unit
 (** [obligation_terminator] part 2 of saving an obligation *)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index bfd7e6b495..31407de4da 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -486,16 +486,11 @@ let save_lemma_admitted ~(lemma : t) : unit =
 (* Saving a lemma-like constant                                         *)
 (************************************************************************)
 
-let finish_proved env sigma opaque idopt po info =
+let finish_proved env sigma idopt po info =
   let open Proof_global in
   let { Info.hook; compute_guard; impargs; other_thms; scope; kind } = info in
   match po with
   | { name; entries=[const]; universes; udecl; poly } ->
-    let is_opaque = match opaque with
-      | Transparent -> false
-      | Opaque      -> true
-    in
-    assert (is_opaque == const.proof_entry_opaque);
     let name = match idopt with
       | None -> name
       | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in
@@ -533,16 +528,16 @@ let finish_proved env sigma opaque idopt po info =
   | _ ->
     CErrors.anomaly Pp.(str "[standard_proof_terminator] close_proof returned more than one proof term")
 
-let finish_derived ~f ~name ~idopt ~opaque ~entries =
+let finish_derived ~f ~name ~idopt ~entries =
   (* [f] and [name] correspond to the proof of [f] and of [suchthat], respectively. *)
 
   if Option.has_some idopt then
     CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.");
 
-  let opaque, f_def, lemma_def =
+  let f_def, lemma_def =
     match entries with
     | [_;f_def;lemma_def] ->
-      opaque <> Proof_global.Transparent , f_def , lemma_def
+      f_def, lemma_def
     | _ -> assert false
   in
   (* The opacity of [f_def] is adjusted to be [false], as it
@@ -568,9 +563,8 @@ let finish_derived ~f ~name ~idopt ~opaque ~entries =
   let lemma_body = Future.chain Proof_global.(lemma_def.proof_entry_body) (fun ((b,ctx),fx) -> (substf b, ctx), fx) in
   let lemma_def = let open Proof_global in
     { lemma_def with
-      proof_entry_body = lemma_body ;
-      proof_entry_type = Some lemma_type ;
-      proof_entry_opaque = opaque ; }
+      proof_entry_body = lemma_body;
+      proof_entry_type = Some lemma_type }
   in
   let lemma_def =
     Declare.DefinitionEntry lemma_def ,
@@ -579,7 +573,7 @@ let finish_derived ~f ~name ~idopt ~opaque ~entries =
   let _ : Names.Constant.t = Declare.declare_constant name lemma_def in
   ()
 
-let finish_proved_equations opaque lid kind proof_obj hook i types wits sigma0 =
+let finish_proved_equations lid kind proof_obj hook i types wits sigma0 =
 
   let open Decl_kinds in
   let obls = ref 1 in
@@ -603,25 +597,25 @@ let finish_proved_equations opaque lid kind proof_obj hook i types wits sigma0 =
   in
   hook recobls sigma
 
-let finalize_proof idopt env sigma opaque proof_obj proof_info =
+let finalize_proof idopt env sigma proof_obj proof_info =
   let open Proof_global in
   let open Proof_ending in
   match CEphemeron.default proof_info.Info.proof_ending Regular with
   | Regular ->
-    finish_proved env sigma opaque idopt proof_obj proof_info
+    finish_proved env sigma idopt proof_obj proof_info
   | End_obligation oinfo ->
-    DeclareObl.obligation_terminator opaque proof_obj.entries proof_obj.universes oinfo
+    DeclareObl.obligation_terminator proof_obj.entries proof_obj.universes oinfo
   | End_derive { f ; name } ->
-    finish_derived ~f ~name ~idopt ~opaque ~entries:proof_obj.entries
+    finish_derived ~f ~name ~idopt ~entries:proof_obj.entries
   | End_equations { hook; i; types; wits; sigma } ->
-    finish_proved_equations opaque idopt proof_info.Info.kind proof_obj hook i types wits sigma
+    finish_proved_equations idopt proof_info.Info.kind proof_obj hook i types wits sigma
 
 let save_lemma_proved ~lemma ~opaque ~idopt =
   (* Env and sigma are just used for error printing in save_remaining_recthms *)
   let env = Global.env () in
   let { Proof.sigma } = Proof.data (Proof_global.get_proof lemma.proof) in
   let proof_obj = Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) lemma.proof in
-  finalize_proof idopt env sigma opaque proof_obj lemma.info
+  finalize_proof idopt env sigma proof_obj lemma.info
 
 (***********************************************************************)
 (* Special case to close a lemma without forcing a proof               *)
@@ -645,8 +639,8 @@ let save_lemma_admitted_delayed ~proof ~info =
   let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in
   finish_admitted env sigma ~name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms
 
-let save_lemma_proved_delayed ~proof ~info ~opaque ~idopt =
+let save_lemma_proved_delayed ~proof ~info ~idopt =
   (* Env and sigma are just used for error printing in save_remaining_recthms *)
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  finalize_proof idopt env sigma opaque proof info
+  finalize_proof idopt env sigma proof info
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 733d84d676..d156954c85 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -148,6 +148,5 @@ val save_lemma_admitted_delayed : proof:Proof_global.proof_object -> info:Info.t
 val save_lemma_proved_delayed
   :  proof:Proof_global.proof_object
   -> info:Info.t
-  -> opaque:Proof_global.opacity_flag
   -> idopt:Names.lident option
   -> unit
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 075de8f3f0..e0183b941e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2778,8 +2778,8 @@ let interp_qed_delayed_proof ~proof ~info ~st ?loc pe : Vernacstate.t =
     let () = match pe with
       | Admitted ->
         save_lemma_admitted_delayed ~proof ~info
-      | Proved (opaque,idopt) ->
-        save_lemma_proved_delayed ~proof ~info ~opaque ~idopt in
+      | Proved (_,idopt) ->
+        save_lemma_proved_delayed ~proof ~info ~idopt in
     { st with Vernacstate.lemmas = stack }
   with exn ->
     let exn = CErrors.push exn in