aboutsummaryrefslogtreecommitdiff
path: root/Control.v
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-12-13 16:23:13 +0100
committerPierre-Marie Pédrot2017-05-19 15:17:31 +0200
commitb5530d8953e74def1feb7dd651ba504e24749055 (patch)
treeb5b9c9a159432c78752e3ca33ba7ab4a25152f70 /Control.v
parent4c5f635769811be7d5f8b39f699b76ea51388cd4 (diff)
Proper handling of exception definition in Ltac2.
We actually implemented a full-fledged open type system, so that exceptions are a special case of it.
Diffstat (limited to 'Control.v')
0 files changed, 0 insertions, 0 deletions