From 24dcc3e2aaa94ac42480c73a6e7e74f8a4aee3fe Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 31 Oct 2019 14:27:37 +0100
Subject: Make [Proof_global.closed_proof_output] opaque

This means return_proof is the only place where it can be produced.

We need to change the stm a bit as it keeps a pointer to a
[closed_proof_output] to join and to check if it failed, and it needs
a way to create a dummy in 1 case.

I'm not sure if this works correctly though, how to test?

We also inline the used bits of [return_proof ~allow_partial:true] in
[save_lemma_admitted] to get [Proof using] info. We could
alternatively expose the [closed_proof_output -> constr list]
projection. I think the code is easier to understand this way though,
as we don't have to read [return_proof] and figure out that the side
effect manipulation is ignored etc.

Note that the "this will warn" comment was outdated since
73daf37ccc7a44cd29c9b67405111756c75cb26a
---
 vernac/lemmas.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'vernac')

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index cf322c52d0..865eded545 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -295,16 +295,18 @@ let save_lemma_admitted ~(lemma : t) : unit =
     | _ -> 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 proof = Proof_global.get_proof lemma.proof in
+  let pproofs = Proof.partial_proof 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, _) :: _ ->
+      | 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
+        (* [pproof] is evar-normalized by [partial_proof]. We don't
+           count variables appearing only in the type of evars. *)
+        let ids_def = Environ.global_vars_set env (EConstr.Unsafe.to_constr pproof) in
         Some (Environ.really_needed env (Id.Set.union ids_typ ids_def))
       | _ -> None in
   let universes = Proof_global.get_initial_euctx lemma.proof in
-- 
cgit v1.2.3