From c6bb30decd15e0d6ef46e14d72472e8ce5dbe627 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 17 Oct 2003 16:06:06 +0000
Subject: Re-desactivation de l'affichage des projections

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4668 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrextern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index afd94b1f63..1be3b805a5 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -58,7 +58,7 @@ let print_universes = ref false
 let print_no_symbol = ref false
 
 (* This governs printing of projections using the dot notation symbols *)
-let print_projections = ref true
+let print_projections = ref false
 
 let print_meta_as_hole = ref false
 
-- 
cgit v1.2.3