aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof_bullet.ml
Commit message (Collapse)AuthorAge
* [proof] Move bullets to their own module.Gravatar Emilio Jesus Gallego Arias2017-06-12
Bullets were placed inside the `Proof_global` module, I guess that due to the global registration function. However, it has logically nothing to do with the functionality of `Proof_global` and the current placement may create some interference between the developers reworking proof state handling and bullets. We thus put the bullet functionality into its own, independent file.