diff options
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. *) |