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
---
 tactics/proof_global.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli
index b9d1b37a11..9161eae82f 100644
--- a/tactics/proof_global.mli
+++ b/tactics/proof_global.mli
@@ -79,7 +79,7 @@ val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.
  * Both access the current proof state. The former is supposed to be
  * chained with a computation that completed the proof *)
 
-type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t
+type closed_proof_output
 
 (* If allow_partial is set (default no) then an incomplete proof
  * is allowed (no error), and a warn is given if the proof is complete. *)
-- 
cgit v1.2.3