aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-01-04 16:16:11 +0100
committerGaëtan Gilbert2019-01-10 16:58:05 +0100
commit723f4434d7c715630533031f1bb1522d5d933ce5 (patch)
treee8dc22422765b7428b29e0634d93e065c87b50c1 /doc/plugin_tutorial
parent2eae13f396833e582697be6a0b3513fc169b8053 (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')
0 files changed, 0 insertions, 0 deletions