aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/db
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>1999-12-14 08:03:32 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>1999-12-14 08:03:32 +0000
commite3be8cdf7c4aa3882028d460267b136dcc36754a (patch)
tree74eb38845328b51c81454487408b7bd3f40fe370 /dev/db
parent0caaf60ee4e6e18fb9d4d36e9d1514914d3bc1ba (diff)
pretty-printers pour le debugger
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@251 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/db')
-rw-r--r--dev/db28
1 files changed, 25 insertions, 3 deletions
diff --git a/dev/db b/dev/db
index 84223c745..2cb7bb5f3 100644
--- a/dev/db
+++ b/dev/db
@@ -1,4 +1,26 @@
-load_printer "db_printers.cmo"
-install_printer Db_printers.prid
-install_printer Db_printers.prsp
+load_printer "top_printers.cmo"
+install_printer Top_printers.prid
+install_printer Top_printers.prsp
+install_printer Top_printers.prast
+install_printer Top_printers.prastpat
+install_printer Top_printers.prastpatl
+
+install_printer Top_printers.pppattern
+install_printer Top_printers.pprawterm
+
+install_printer Top_printers.ppterm0
+install_printer Top_printers.print_uni
+install_printer Top_printers.pp_universes
+install_printer Top_printers.pptype
+install_printer Top_printers.prj
+
+install_printer Top_printers.prgoal
+install_printer Top_printers.prsigmagoal
+install_printer Top_printers.prctxt
+install_printer Top_printers.pproof
+install_printer Top_printers.prevd
+install_printer Top_printers.prevc
+install_printer Top_printers.prwc
+install_printer Top_printers.prclenv
+