From b1cd93c7ad0f550077a62a1c7cb6915041c6c85e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 7 Mar 2017 16:21:10 +0100
Subject: Turning the printing primitive projection compatibility flag off by
 default.

---
 doc/refman/RefMan-ext.tex | 2 +-
 pretyping/detyping.ml     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 1d423f8b16..162cfdba41 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -321,7 +321,7 @@ for the usual defined ones.
 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 {\tt Printing Primitive Projection Parameters}
-flag. Further compatibility printing can be deactivated thanks to the
+flag. Further compatibility printing can be activated thanks to the
 {\tt Printing Primitive Projection Compatibility} option which governs the
 printing of pattern-matching over primitive records.
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 5a296de84b..bf1e0e040f 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -173,7 +173,7 @@ let _ = declare_bool_option
 	    optread  = print_primproj_params;
 	    optwrite = (:=) print_primproj_params_value }
 
-let print_primproj_compatibility_value = ref true
+let print_primproj_compatibility_value = ref false
 let print_primproj_compatibility () = !print_primproj_compatibility_value
 
 let _ = declare_bool_option
-- 
cgit v1.2.3


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 +++---
 pretyping/detyping.ml     | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

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.
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index bf1e0e040f..0b5ea86d5d 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -162,7 +162,7 @@ let _ = declare_bool_option
 	    optread  = reverse_matching;
 	    optwrite = (:=) reverse_matching_value }
 
-let print_primproj_params_value = ref true
+let print_primproj_params_value = ref false
 let print_primproj_params () = !print_primproj_params_value
 
 let _ = declare_bool_option
-- 
cgit v1.2.3