From c939260137bef6002aad416632641c04601dc2b8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 22 Jan 2007 15:05:59 +0000
Subject: Allègement de l'affichage des références par le printer si possible
 (on garde des noms de la forme IND(name,i) et CONSTR(name,i,j) que lorsqu'on
 ne sait pas le bon nom, i.e. pour les IND mutuels autres que le premier et
 pour tous les constructeurs). Pour un affichage complètement explicite des
 noms avec ocamldebug, charger maintenant set_raw_db en plus de db.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9515 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/set_raw_db      | 1 +
 dev/top_printers.ml | 3 ++-
 2 files changed, 3 insertions(+), 1 deletion(-)
 create mode 100644 dev/set_raw_db

(limited to 'dev')

diff --git a/dev/set_raw_db b/dev/set_raw_db
new file mode 100644
index 0000000000..5caff7e5d4
--- /dev/null
+++ b/dev/set_raw_db
@@ -0,0 +1 @@
+install_printer Top_printers.ppconstrdb
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index df089f0b1b..df3835d2fe 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -46,7 +46,8 @@ let ppsp sp = pp(pr_sp sp)
 let ppqualid qid = pp(pr_qualid qid)
 
 (* term printers *)
-let ppconstr x = pp(Termops.print_constr x)
+let ppconstr x = pp (Termops.print_constr x)
+let ppconstrdb x = pp(Options.with_option Constrextern.rawdebug Termops.print_constr x)
 let ppterm = ppconstr
 let ppsconstr x = ppconstr (Declarations.force x)
 let ppconstr_univ x = Constrextern.with_universes ppconstr x
-- 
cgit v1.2.3