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`.
---
 doc/sphinx/language/gallina-extensions.rst | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 376a6b8eed..dec4b1a38a 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -246,11 +246,6 @@ Primitive Projections
    printing time (even though they are absent in the actual AST manipulated
    by the kernel).
 
-.. flag:: Printing Primitive Projection Compatibility
-
-   This compatibility option (on by default) governs the
-   printing of pattern matching over primitive records.
-
 Primitive Record Types
 ++++++++++++++++++++++
 
@@ -296,8 +291,8 @@ the folded version delta-reduces to the unfolded version. This allows to
 precisely mimic the usual unfolding rules of constants. Projections
 obey the usual ``simpl`` flags of the ``Arguments`` command in particular.
 There is currently no way to input unfolded primitive projections at the
-user-level, and one must use the :flag:`Printing Primitive Projection Compatibility`
-to display unfolded primitive projections as matches and distinguish them from folded ones.
+user-level, and there is no way to display unfolded projections differently
+from folded ones.
 
 
 Compatibility Projections and :g:`match`
-- 
cgit v1.2.3