diff options
| author | Pierre-Marie Pédrot | 2018-07-11 22:57:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-12 13:53:22 +0200 |
| commit | b9ff36b39eb193757ce57a89afe138cd09e759d7 (patch) | |
| tree | 5c692d9cad8ce9db00c9d7c127750650cd7b26a8 /kernel/nativeconv.ml | |
| parent | 270ceed48217797e99ec845cc5d1c599b5729bc2 (diff) | |
Statically typecheck the VERNAC EXTEND wrapper.
This moves the typing code from the macro expansion to the extension
registering mechanism, bringing in more static safety. We also seize
the opportunity to remove dead code in the macro.
Diffstat (limited to 'kernel/nativeconv.ml')
0 files changed, 0 insertions, 0 deletions