diff options
Diffstat (limited to 'proofs/proof.ml')
| -rw-r--r-- | proofs/proof.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 413b5fdd7..04e707cd6 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -98,7 +98,7 @@ let done_cond ?(loose_end=false) k = CondDone (loose_end,k) (* Subpart of the type of proofs. It contains the parts of the proof which are under control of the undo mechanism *) -type proof = { +type t = { (* Current focused proofview *) proofview: Proofview.proofview; (* Entry for the proofview *) @@ -115,6 +115,8 @@ type proof = { initial_euctx : UState.t } +type proof = t + (*** General proof functions ***) let proof p = |