aboutsummaryrefslogtreecommitdiff
path: root/stm/proofBlockDelimiter.mli
AgeCommit message (Collapse)Author
2016-06-06STM: proof block detection for par:Enrico Tassi
"par: tac" is a terminator, if it fails we can admit all focused goals and continue.
2016-06-06STM: proof block detection for bullets and { block }Enrico Tassi