diff options
Diffstat (limited to 'proofs/proof_bullet.ml')
| -rw-r--r-- | proofs/proof_bullet.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index 5702156b65..66e2ae5c29 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -50,7 +50,7 @@ module Strict = struct | Suggest of t (* this bullet is mandatory here *) | Unfinished of t (* no mandatory bullet here, but this bullet is unfinished *) | NoBulletInUse (* No mandatory bullet (or brace) here, no bullet pending, - some focused goals exists. *) + some focused goals exists. *) | NeedClosingBrace (* Some unfocussed goal exists "{" needed to focus them *) | ProofFinished (* No more goal anywhere *) |