diff options
| author | Gaëtan Gilbert | 2019-01-04 16:16:11 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-10 16:58:05 +0100 |
| commit | 723f4434d7c715630533031f1bb1522d5d933ce5 (patch) | |
| tree | e8dc22422765b7428b29e0634d93e065c87b50c1 /doc/plugin_tutorial/tuto3 | |
| parent | 2eae13f396833e582697be6a0b3513fc169b8053 (diff) | |
Remove Printing Primitive Projection Compatibility
The code to generate the legacy bodies is moved to its only user in
extraction.
It almost seems like we could remove it (ie no special extraction code
for primitive projection constants) but then we run into issues with
automatic unboxing eg `Record foo := { a : nat; b : a <= 5 }.` gets
extracted to `type foo = nat` and (if we remove the special code) `let
a = a`.
Diffstat (limited to 'doc/plugin_tutorial/tuto3')
0 files changed, 0 insertions, 0 deletions
