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.

---
 pretyping/detyping.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

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