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 /test-suite | |
| 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 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_5197.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/bug_5197.v b/test-suite/bugs/closed/bug_5197.v index b67e93d677..0c236e12ad 100644 --- a/test-suite/bugs/closed/bug_5197.v +++ b/test-suite/bugs/closed/bug_5197.v @@ -1,6 +1,6 @@ Set Universe Polymorphism. Set Primitive Projections. -Unset Printing Primitive Projection Compatibility. + Axiom Ω : Type. Record Pack (A : Ω -> Type) (Aᴿ : Ω -> (forall ω : Ω, A ω) -> Type) := mkPack { |