From d9552de21522f19f7656a6b635dee1e325262e09 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 4 Jan 2006 16:33:53 +0000
Subject: Affichage concis des locations (si jamais ppterm/pprawterm sont
 débranchés)

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

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index e74154b099..55e2c92863 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -36,7 +36,7 @@
 #install_printer ppwhd;;
 #install_printer ppvblock;;
 #install_printer  (* bigint *) ppbigint;;
-
+#install_printer  (* loc *) pploc;;
 
 let qid = Libnames.qualid_of_string;;
 
-- 
cgit v1.2.3