aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.ml
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 /kernel/type_errors.ml
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 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions