diff options
| author | Gaëtan Gilbert | 2019-10-31 14:27:37 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-11-08 16:29:16 +0100 |
| commit | 24dcc3e2aaa94ac42480c73a6e7e74f8a4aee3fe (patch) | |
| tree | d0a8d17b85df7fff7e3dba7f58bd3a9bc58985df /tactics | |
| parent | f70ec9d4279f7b4b943eb28f15d6e4244bb82fc5 (diff) | |
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
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/proof_global.mli | 2 |
1 files changed, 1 insertions, 1 deletions
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. *) |