From 514a4db2eca54ae8c4c1ba1e081a918528566fce Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Mon, 5 Aug 2019 12:11:48 -0700
Subject: Remove reference to removed option Printing Primitive Projection
 Compatibility

---
 doc/sphinx/language/gallina-extensions.rst | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index acf68e9fd2..dc4f91e66b 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -260,10 +260,7 @@ To eliminate the (co-)inductive type, one must use its defined primitive project
 For compatibility, the parameters still appear to the user when
 printing terms even though they are absent in the actual AST
 manipulated by the kernel. This can be changed by unsetting the
-:flag:`Printing Primitive Projection Parameters` flag. Further compatibility
-printing can be deactivated thanks to the ``Printing Primitive Projection
-Compatibility`` option which governs the printing of pattern matching
-over primitive records.
+:flag:`Printing Primitive Projection Parameters` flag.
 
 There are currently two ways to introduce primitive records types:
 
-- 
cgit v1.2.3