aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar Arnaud Spiwack <arnaud@spiwack.net>2013-11-26 11:53:09 +0100
committerGravatar Arnaud Spiwack <arnaud@spiwack.net>2013-12-04 14:14:32 +0100
commitdb65876404c7c3a1343623cc9b4d6c2a7164dd95 (patch)
tree2f73652c1014775aa0fc171f9a64a8807ede7ac5 /proofs
parenteef907ed0a200e912ab2eddc0fcea41b5f61c145 (diff)
Vernac classification: allow for commands which start proofs but must be synchrone.
The previous heuristic is to check whether the proof ends with Qed or not. This modification allows for commands which start proof but may produce transparent term even when the function ends with Qed.
Diffstat (limited to 'proofs')
0 files changed, 0 insertions, 0 deletions