diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-01-04 16:33:53 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-01-04 16:33:53 +0000 |
commit | d9552de21522f19f7656a6b635dee1e325262e09 (patch) | |
tree | 5ef2b74415a94d78371d24da9813b9a8fd753512 /dev | |
parent | 6552e154318f590336ae2226ba615b9e4cca0608 (diff) |
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
Diffstat (limited to 'dev')
-rw-r--r-- | dev/base_include | 2 | ||||
-rw-r--r-- | dev/db | 4 |
2 files changed, 4 insertions, 2 deletions
diff --git a/dev/base_include b/dev/base_include index e74154b09..55e2c9286 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;; @@ -29,5 +29,7 @@ install_printer Top_printers.prevd install_printer Top_printers.prclenv install_printer Top_printers.pptac -install_printer Top_printers.pr_obj +install_printer Top_printers.pr_obj +install_printer Top_printers.pploc + |