diff options
| author | Pierre-Marie Pédrot | 2016-12-13 16:23:13 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-05-19 15:17:31 +0200 |
| commit | b5530d8953e74def1feb7dd651ba504e24749055 (patch) | |
| tree | b5b9c9a159432c78752e3ca33ba7ab4a25152f70 /String.v | |
| parent | 4c5f635769811be7d5f8b39f699b76ea51388cd4 (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 'String.v')
0 files changed, 0 insertions, 0 deletions