From 723f4434d7c715630533031f1bb1522d5d933ce5 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 4 Jan 2019 16:16:11 +0100
Subject: 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`.
---
 test-suite/bugs/closed/bug_5197.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

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 {
-- 
cgit v1.2.3