diff options
| author | herbelin | 2006-01-04 16:33:53 +0000 |
|---|---|---|
| committer | herbelin | 2006-01-04 16:33:53 +0000 |
| commit | d9552de21522f19f7656a6b635dee1e325262e09 (patch) | |
| tree | 5ef2b74415a94d78371d24da9813b9a8fd753512 /dev/base_include | |
| 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/base_include')
| -rw-r--r-- | dev/base_include | 2 |
1 files changed, 1 insertions, 1 deletions
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;; |