aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/proofBlockDelimiter.mli
Commit message (Collapse)AuthorAge
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* STM: proof block detection for par:Gravatar Enrico Tassi2016-06-06
| | | | | "par: tac" is a terminator, if it fails we can admit all focused goals and continue.
* STM: proof block detection for bullets and { block }Gravatar Enrico Tassi2016-06-06