From d4aeb1ef92a9fc35b242a0d91488de60c24d7bbb Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 7 Jun 2019 15:22:31 +0200
Subject: [stm] [vernac] Remove special ?proof parameter from vernac main path

We move special vernac-qed handling to a special function, making the
regular vernacular interpretation path uniform.

This is an important step as it paves the way up to export the vernac
DSL to clients, as there are no special vernacs anymore in the regular
interp path, except for Load, which should be handled separately due
to silly reasons, as morally it is a `VtNoProof` command.
---
 vernac/lemmas.ml         | 131 +++++++++++++++++++++++------------------------
 vernac/lemmas.mli        |  26 +++++-----
 vernac/vernacentries.ml  |  68 ++++++++++++------------
 vernac/vernacentries.mli |  15 ++++--
 4 files changed, 121 insertions(+), 119 deletions(-)

(limited to 'vernac')

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 35b902fff9..bfd7e6b495 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -455,54 +455,32 @@ let finish_admitted env sigma ~name ~poly ~scope pe ctx hook ~udecl impargs othe
   process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (ConstRef kn) impargs other_thms;
   Feedback.feedback Feedback.AddedAxiom
 
-let save_lemma_admitted ?proof ~(lemma : t) =
-    let open Proof_global in
-    let env = Global.env () in
-    match proof with
-    | Some ({ name; entries; universes; udecl }, { Info.hook; scope; impargs; other_thms; _} ) ->
-      if List.length entries <> 1 then
-        user_err Pp.(str "Admitted does not support multiple statements");
-      let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
-      if proof_entry_type = None then
-        user_err Pp.(str "Admitted requires an explicit statement");
-      let poly = match proof_entry_universes with
-        | Entries.Monomorphic_entry _ -> false
-        | Entries.Polymorphic_entry (_, _) -> true in
-      let typ = Option.get proof_entry_type in
-      let ctx = UState.univ_entry ~poly universes in
-      let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in
-      let sigma = Evd.from_env env in
-      finish_admitted env sigma ~name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms
-    | None ->
-      let pftree = Proof_global.get_proof lemma.proof in
-      let scope = lemma.info.Info.scope in
-      let Proof.{ name; poly; entry } = Proof.data pftree in
-      let typ = match Proofview.initial_goals entry with
-        | [typ] -> snd typ
-        | _ ->
-          CErrors.anomaly
-            ~label:"Lemmas.save_proof" (Pp.str "more than one statement.")
-      in
-      let typ = EConstr.Unsafe.to_constr typ in
-      let universes = Proof_global.get_initial_euctx lemma.proof in
-      (* This will warn if the proof is complete *)
-      let pproofs, _univs =
-        Proof_global.return_proof ~allow_partial:true lemma.proof in
-      let sec_vars =
-        if not (get_keep_admitted_vars ()) then None
-        else match Proof_global.get_used_variables lemma.proof, pproofs with
-          | Some _ as x, _ -> x
-          | None, (pproof, _) :: _ ->
-            let env = Global.env () in
-            let ids_typ = Environ.global_vars_set env typ in
-            let ids_def = Environ.global_vars_set env pproof in
-            Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def))
-          | _ -> None in
-      let udecl = Proof_global.get_universe_decl lemma.proof in
-      let { Info.hook; impargs; other_thms } = lemma.info in
-      let { Proof.sigma } = Proof.data (Proof_global.get_proof lemma.proof) in
-      let ctx = UState.check_univ_decl ~poly universes udecl in
-      finish_admitted env sigma ~name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms
+let save_lemma_admitted ~(lemma : t) : unit =
+  (* Used for printing in recthms *)
+  let env = Global.env () in
+  let { Info.hook; scope; impargs; other_thms } = lemma.info in
+  let udecl = Proof_global.get_universe_decl lemma.proof in
+  let Proof.{ sigma; name; poly; entry } = Proof.data (Proof_global.get_proof lemma.proof) in
+  let typ = match Proofview.initial_goals entry with
+    | [typ] -> snd typ
+    | _ -> CErrors.anomaly ~label:"Lemmas.save_proof" (Pp.str "more than one statement.")
+  in
+  let typ = EConstr.Unsafe.to_constr typ in
+  (* This will warn if the proof is complete *)
+  let pproofs, _univs = Proof_global.return_proof ~allow_partial:true lemma.proof in
+  let sec_vars =
+    if not (get_keep_admitted_vars ()) then None
+    else match Proof_global.get_used_variables lemma.proof, pproofs with
+      | Some _ as x, _ -> x
+      | None, (pproof, _) :: _ ->
+        let env = Global.env () in
+        let ids_typ = Environ.global_vars_set env typ in
+        let ids_def = Environ.global_vars_set env pproof in
+        Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def))
+      | _ -> None in
+  let universes = Proof_global.get_initial_euctx lemma.proof in
+  let ctx = UState.check_univ_decl ~poly universes udecl in
+  finish_admitted env sigma ~name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms
 
 (************************************************************************)
 (* Saving a lemma-like constant                                         *)
@@ -598,7 +576,8 @@ let finish_derived ~f ~name ~idopt ~opaque ~entries =
     Declare.DefinitionEntry lemma_def ,
     Decl_kinds.(IsProof Proposition)
   in
-  ignore (Declare.declare_constant name lemma_def)
+  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 =
 
@@ -624,24 +603,7 @@ let finish_proved_equations opaque lid kind proof_obj hook i types wits sigma0 =
   in
   hook recobls sigma
 
-let save_lemma_proved ?proof ?lemma ~opaque ~idopt =
-  (* Invariant (uh) *)
-  if Option.is_empty lemma && Option.is_empty proof then
-    user_err (str "No focused proof (No proof-editing in progress).");
-  (* Env and sigma are just used for error printing in save_remaining_recthms *)
-  let env = Global.env () in
-  let sigma, proof_obj, proof_info =
-    match proof with
-    | None ->
-      (* XXX: The close_proof and proof state API should be refactored
-         so it is possible to insert proofs properly into the state *)
-      let { proof; info } = Option.get lemma in
-      let { Proof.sigma } = Proof.data (Proof_global.get_proof proof) in
-      sigma,
-      Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, info
-    | Some (proof, info) ->
-      Evd.from_env env, proof, info
-  in
+let finalize_proof idopt env sigma opaque proof_obj proof_info =
   let open Proof_global in
   let open Proof_ending in
   match CEphemeron.default proof_info.Info.proof_ending Regular with
@@ -653,3 +615,38 @@ let save_lemma_proved ?proof ?lemma ~opaque ~idopt =
     finish_derived ~f ~name ~idopt ~opaque ~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
+
+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
+
+(***********************************************************************)
+(* Special case to close a lemma without forcing a proof               *)
+(***********************************************************************)
+let save_lemma_admitted_delayed ~proof ~info =
+  let open Proof_global in
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let { name; entries; universes; udecl; poly } = proof in
+  let { Info.hook; scope; impargs; other_thms } = info in
+  if List.length entries <> 1 then
+    user_err Pp.(str "Admitted does not support multiple statements");
+  let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
+  let poly = match proof_entry_universes with
+    | Entries.Monomorphic_entry _ -> false
+    | Entries.Polymorphic_entry (_, _) -> true in
+  let typ = match proof_entry_type with
+    | None -> user_err Pp.(str "Admitted requires an explicit statement");
+    | Some typ -> typ in
+  let ctx = UState.univ_entry ~poly universes in
+  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 =
+  (* 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
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 276d7ae144..733d84d676 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -129,21 +129,9 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val
 
 (** {4 Saving proofs} *)
 
-(** The extra [?proof] parameter here is due to problems with the
-    lower-level [Proof_global.close_proof] API; we cannot inject closed
-    proofs properly in the proof state so we must leave this backdoor open.
-
-    The regular user can ignore it.
-*)
-
-val save_lemma_admitted
-  :  ?proof:(Proof_global.proof_object * Info.t)
-  -> lemma:t
-  -> unit
-
+val save_lemma_admitted : lemma:t -> unit
 val save_lemma_proved
-  :  ?proof:(Proof_global.proof_object * Info.t)
-  -> ?lemma:t
+  :  lemma:t
   -> opaque:Proof_global.opacity_flag
   -> idopt:Names.lident option
   -> unit
@@ -153,3 +141,13 @@ module Internal : sig
   val get_info : t -> Info.t
   (** Only needed due to the Proof_global compatibility layer. *)
 end
+
+(** Special cases for delayed proofs, in this case we must provide the
+   proof information so the proof won't be forced. *)
+val save_lemma_admitted_delayed : proof:Proof_global.proof_object -> info:Info.t -> unit
+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 2bcd06b4d9..075de8f3f0 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -47,16 +47,6 @@ let vernac_pperr_endline pp =
    instead enviroment/state selection should be done at the Vernac DSL
    level. *)
 
-(* EJGA: Only used in close_proof, can remove once the ?proof hack is no more *)
-let vernac_require_open_lemma ~stack f =
-  match stack with
-  | Some stack -> f ~stack
-  | None -> user_err Pp.(str "Command not supported (No proof-editing in progress)")
-
-let with_pstate ~stack f =
-  vernac_require_open_lemma ~stack
-    (fun ~stack -> Vernacstate.LemmaStack.with_top_pstate stack ~f:(fun pstate -> f ~pstate))
-
 let get_current_or_global_context ~pstate =
   match pstate with
   | None -> let env = Global.env () in Evd.(from_env env, env)
@@ -642,27 +632,17 @@ let vernac_start_proof ~atts kind l =
     List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
   start_proof_and_print ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Proof kind) l
 
-let vernac_end_proof ?stack ?proof = let open Vernacexpr in function
+let vernac_end_proof ~lemma = let open Vernacexpr in function
   | Admitted ->
-    vernac_require_open_lemma ~stack (fun ~stack ->
-      let lemma, stack = Vernacstate.LemmaStack.pop stack in
-      save_lemma_admitted ?proof ~lemma;
-      stack)
+    save_lemma_admitted ~lemma
   | Proved (opaque,idopt) ->
-    let lemma, stack = match stack with
-      | None -> None, None
-      | Some stack ->
-        let lemma, stack = Vernacstate.LemmaStack.pop stack in
-        Some lemma, stack
-    in
-    save_lemma_proved ?lemma ?proof ~opaque ~idopt;
-    stack
+    save_lemma_proved ~lemma ~opaque ~idopt
 
 let vernac_exact_proof ~lemma c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the beginning of a proof. *)
   let lemma, status = Lemmas.by (Tactics.exact_proof c) lemma in
-  let () = save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Opaque ~idopt:None in
+  let () = save_lemma_proved ~lemma ~opaque:Proof_global.Opaque ~idopt:None in
   if not status then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_assumption ~atts discharge kind l nl =
@@ -2324,6 +2304,12 @@ let locate_if_not_already ?loc (e, info) =
 
 exception End_of_input
 
+(* EJGA: We may remove this, only used twice below *)
+let vernac_require_open_lemma ~stack f =
+  match stack with
+  | Some stack -> f stack
+  | None -> user_err Pp.(str "Command not supported (No proof-editing in progress)")
+
 let interp_typed_vernac c ~stack =
   let open Vernacextend in
   match c with
@@ -2334,7 +2320,7 @@ let interp_typed_vernac c ~stack =
     let () = f () in
     stack
   | VtCloseProof f ->
-    vernac_require_open_lemma ~stack (fun ~stack ->
+    vernac_require_open_lemma ~stack (fun stack ->
         let lemma, stack = Vernacstate.LemmaStack.pop stack in
         f ~lemma;
         stack)
@@ -2347,13 +2333,13 @@ let interp_typed_vernac c ~stack =
     f ~pstate;
     stack
   | VtReadProof f ->
-    with_pstate ~stack f;
+    vernac_require_open_lemma ~stack
+      (Vernacstate.LemmaStack.with_top_pstate ~f:(fun pstate -> f ~pstate));
     stack
 
 (* We interpret vernacular commands to a DSL that specifies their
    allowed actions on proof states *)
 let translate_vernac ~atts v = let open Vernacextend in match v with
-  | VernacEndProof _
   | VernacAbortAll
   | VernacRestart
   | VernacUndo _
@@ -2664,6 +2650,9 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
   | VernacProofMode mn ->
     VtDefault(fun () -> unsupported_attributes atts)
 
+  | VernacEndProof pe ->
+    VtCloseProof (vernac_end_proof pe)
+
   (* Extensions *)
   | VernacExtend (opn,args) ->
     Vernacextend.type_vernac ~atts opn args
@@ -2698,11 +2687,6 @@ let rec interp_expr ?proof ~atts ~st c =
     unsupported_attributes atts;
     vernac_load ~verbosely ~st fname
 
-  (* Special: ?proof parameter doesn't allow for uniform pstate pop :S *)
-  | VernacEndProof e ->
-    unsupported_attributes atts;
-    vernac_end_proof ?proof ?stack e
-
   | v ->
     let fv = translate_vernac ~atts v in
     interp_typed_vernac ~stack fv
@@ -2773,11 +2757,11 @@ let () =
       optwrite = ((:=) default_timeout) }
 
 (* Be careful with the cache here in case of an exception. *)
-let interp ?(verbosely=true) ?proof ~st cmd =
+let interp ?(verbosely=true) ~st cmd =
   Vernacstate.unfreeze_interp_state st;
   try vernac_timeout (fun st ->
       let v_mod = if verbosely then Flags.verbosely else Flags.silently in
-      let ontop = v_mod (interp_control ?proof ~st) cmd in
+      let ontop = v_mod (interp_control ~st) cmd in
       Vernacstate.Proof_global.set ontop [@ocaml.warning "-3"];
       Vernacstate.freeze_interp_state ~marshallable:false
     ) st
@@ -2786,3 +2770,19 @@ let interp ?(verbosely=true) ?proof ~st cmd =
     let exn = locate_if_not_already ?loc:cmd.CAst.loc exn in
     Vernacstate.invalidate_cache ();
     iraise exn
+
+let interp_qed_delayed_proof ~proof ~info ~st ?loc pe : Vernacstate.t =
+  let stack = st.Vernacstate.lemmas in
+  let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in
+  try
+    let () = match pe with
+      | Admitted ->
+        save_lemma_admitted_delayed ~proof ~info
+      | Proved (opaque,idopt) ->
+        save_lemma_proved_delayed ~proof ~info ~opaque ~idopt in
+    { st with Vernacstate.lemmas = stack }
+  with exn ->
+    let exn = CErrors.push exn in
+    let exn = locate_if_not_already ?loc exn in
+    Vernacstate.invalidate_cache ();
+    iraise exn
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index ad3e9f93d9..3563e9984a 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -20,10 +20,17 @@ val vernac_require :
   Libnames.qualid option -> bool option -> Libnames.qualid list -> unit
 
 (** The main interpretation function of vernacular expressions *)
-val interp :
-  ?verbosely:bool ->
-  ?proof:(Proof_global.proof_object * Lemmas.Info.t) ->
-  st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t
+val interp : ?verbosely:bool -> st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t
+
+(** Execute a Qed but with a proof_object which may contain a delayed
+   proof and won't be forced *)
+val interp_qed_delayed_proof
+  :  proof:Proof_global.proof_object
+  -> info:Lemmas.Info.t
+  -> st:Vernacstate.t
+  -> ?loc:Loc.t
+  -> Vernacexpr.proof_end
+  -> Vernacstate.t
 
 (** Prepare a "match" template for a given inductive type.
     For each branch of the match, we list the constructor name
-- 
cgit v1.2.3


From 132de86d82dbf186ea645f704f699c00b505704b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 26 Jun 2019 12:12:44 +0200
Subject: [proof] finalize_proof doesn't need opaque (it's already in entries)

---
 vernac/declareObl.ml    | 14 +++++++-------
 vernac/declareObl.mli   |  3 +--
 vernac/lemmas.ml        | 36 +++++++++++++++---------------------
 vernac/lemmas.mli       |  1 -
 vernac/vernacentries.ml |  4 ++--
 5 files changed, 25 insertions(+), 33 deletions(-)

(limited to 'vernac')

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
-- 
cgit v1.2.3