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.

---
 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 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