aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/db
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-01-11 09:47:32 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-01-11 09:47:32 +0000
commitdcaefd4a668617504aaf335ed346598b03a80ba1 (patch)
tree9b97ca322252777d101152452193d0a7c8537e2e /dev/db
parent88d15de0cc467368dc71851e995d82093f9692ca (diff)
Restructuration et simplification des fonctions d'affichage, de détypage
et d'"externalisation"; standardisation du nom des fonctions d'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/db')
-rw-r--r--dev/db40
1 files changed, 20 insertions, 20 deletions
diff --git a/dev/db b/dev/db
index 54e0706cc..751043977 100644
--- a/dev/db
+++ b/dev/db
@@ -1,35 +1,35 @@
load_printer "gramlib.cma"
load_printer "printers.cma"
-install_printer Top_printers.prid
-install_printer Top_printers.prlab
-install_printer Top_printers.prmsid
-install_printer Top_printers.prmbid
-install_printer Top_printers.prdir
-install_printer Top_printers.prmp
-install_printer Top_printers.prkn
-install_printer Top_printers.prcon
-install_printer Top_printers.prsp
-install_printer Top_printers.prqualid
+install_printer Top_printers.ppid
+install_printer Top_printers.pplab
+install_printer Top_printers.ppmsid
+install_printer Top_printers.ppmbid
+install_printer Top_printers.ppdir
+install_printer Top_printers.ppmp
+install_printer Top_printers.ppkn
+install_printer Top_printers.ppcon
+install_printer Top_printers.ppsp
+install_printer Top_printers.ppqualid
install_printer Top_printers.ppbigint
install_printer Top_printers.pppattern
-install_printer Top_printers.pprawterm
+install_printer Top_printers.pprawconstr
-install_printer Top_printers.ppterm
-install_printer Top_printers.print_uni
-install_printer Top_printers.pp_universes
+install_printer Top_printers.ppconstr
+install_printer Top_printers.ppuni
+install_printer Top_printers.ppuniverses
install_printer Top_printers.pptype
-install_printer Top_printers.prj
+install_printer Top_printers.ppj
-install_printer Top_printers.prgoal
-install_printer Top_printers.prsigmagoal
+install_printer Top_printers.ppgoal
+install_printer Top_printers.ppsigmagoal
install_printer Top_printers.pproof
-install_printer Top_printers.prevd
-install_printer Top_printers.prclenv
+install_printer Top_printers.ppevd
+install_printer Top_printers.ppclenv
install_printer Top_printers.pptac
-install_printer Top_printers.pr_obj
+install_printer Top_printers.ppobj
install_printer Top_printers.pploc