diff options
| author | herbelin | 2007-01-22 15:05:59 +0000 |
|---|---|---|
| committer | herbelin | 2007-01-22 15:05:59 +0000 |
| commit | c939260137bef6002aad416632641c04601dc2b8 (patch) | |
| tree | 0d5ff0a50600d8b4faf06bbb7bb1e35367af9e42 /dev | |
| parent | 55606828d6d6790631908b33dd9b13373a7ed096 (diff) | |
Allègement de l'affichage des références par le printer si possible
(on garde des noms de la forme IND(name,i) et CONSTR(name,i,j) que
lorsqu'on ne sait pas le bon nom, i.e. pour les IND mutuels autres que
le premier et pour tous les constructeurs).
Pour un affichage complètement explicite des noms avec ocamldebug,
charger maintenant set_raw_db en plus de db.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9515 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/set_raw_db | 1 | ||||
| -rw-r--r-- | dev/top_printers.ml | 3 |
2 files changed, 3 insertions, 1 deletions
diff --git a/dev/set_raw_db b/dev/set_raw_db new file mode 100644 index 0000000000..5caff7e5d4 --- /dev/null +++ b/dev/set_raw_db @@ -0,0 +1 @@ +install_printer Top_printers.ppconstrdb diff --git a/dev/top_printers.ml b/dev/top_printers.ml index df089f0b1b..df3835d2fe 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -46,7 +46,8 @@ let ppsp sp = pp(pr_sp sp) let ppqualid qid = pp(pr_qualid qid) (* term printers *) -let ppconstr x = pp(Termops.print_constr x) +let ppconstr x = pp (Termops.print_constr x) +let ppconstrdb x = pp(Options.with_option Constrextern.rawdebug Termops.print_constr x) let ppterm = ppconstr let ppsconstr x = ppconstr (Declarations.force x) let ppconstr_univ x = Constrextern.with_universes ppconstr x |