aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto1
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-09-09 02:02:52 +0200
committerPierre-Marie Pédrot2017-09-09 02:09:20 +0200
commit0ece31492e4cf2813025aab3c4972bb769a3dea2 (patch)
treebf610456520c27f992f26166c534402104b6cc43 /doc/plugin_tutorial/tuto1
parent555a7cf0ce4457ecfbf68cd12dd0e801728f6662 (diff)
Fix coq/ltac2#25: Control.case should not be able to catch Control.throw.
When crossing constr boundaries, we mark exceptions as being fatal not to catch them.
Diffstat (limited to 'doc/plugin_tutorial/tuto1')
0 files changed, 0 insertions, 0 deletions