From bd76257f84dcaef90498a85342077a743855f565 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 3 Apr 2017 15:59:48 +0200
Subject: Turning the printing primitive projection parameter flag off by
 default.

---
 doc/refman/RefMan-ext.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 162cfdba41..9ef5267e21 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -318,10 +318,10 @@ for the usual defined ones.
   % - [pattern x at n], [rewrite x at n] and in general abstraction and selection
   %   of occurrences may fail due to the disappearance of parameters.
 
-For compatibility, the parameters still appear to the user when printing terms
+The internally omitted parameters can be reconstructed at printing time
 even though they are absent in the actual AST manipulated by the kernel. This
-can be changed by unsetting the {\tt Printing Primitive Projection Parameters}
-flag. Further compatibility printing can be activated thanks to the
+can be obtained by setting the {\tt Printing Primitive Projection Parameters}
+flag. Another compatibility printing can be activated thanks to the
 {\tt Printing Primitive Projection Compatibility} option which governs the
 printing of pattern-matching over primitive records.
 
-- 
cgit v1.2.3