diff options
| author | herbelin | 2006-01-11 09:47:32 +0000 |
|---|---|---|
| committer | herbelin | 2006-01-11 09:47:32 +0000 |
| commit | dcaefd4a668617504aaf335ed346598b03a80ba1 (patch) | |
| tree | 9b97ca322252777d101152452193d0a7c8537e2e /dev/base_include | |
| parent | 88d15de0cc467368dc71851e995d82093f9692ca (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/base_include')
| -rw-r--r-- | dev/base_include | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/dev/base_include b/dev/base_include index 55e2c92863..cd837ab6a6 100644 --- a/dev/base_include +++ b/dev/base_include @@ -17,16 +17,16 @@ #use "top_printers.ml";; #use "vm_printers.ml";; -#install_printer (* identifier *) prid;; -#install_printer (* label *) prlab;; -#install_printer prmsid;; -#install_printer prmbid;; -#install_printer prdir;; -#install_printer prmp;; -#install_printer (* section_path *) prsp;; -#install_printer (* qualid *) prqualid;; -#install_printer (* kernel_name *) prkn;; -#install_printer (* constant *) prcon;; +#install_printer (* identifier *) ppid;; +#install_printer (* label *) pplab;; +#install_printer (* mod_self_id *) ppmsid;; +#install_printer (* mod_bound_id *) ppmbid;; +#install_printer (* dir_path *) ppdir;; +#install_printer (* module_path *) ppmp;; +#install_printer (* section_path *) ppsp;; +#install_printer (* qualid *) ppqualid;; +#install_printer (* kernel_name *) ppkn;; +#install_printer (* constant *) ppcon;; #install_printer (* constr *) print_pure_constr;; #install_printer (* patch *) ppripos;; #install_printer (* values *) ppvalues;; |