coq/dev/set_raw_db, branch master The formal proof system Cleanup debug printers a bit, add generated mli. 2017-12-22T15:36:32+00:00 Gaëtan Gilbert 2017-12-16T09:58:52+00:00 87cbd64254f33439882156d9a297a6a2f6886057 






Allègement de l'affichage des références par le printer si possible
2007-01-22T15:05:59+00:00

herbelin

2007-01-22T15:05:59+00:00

c939260137bef6002aad416632641c04601dc2b8

(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





(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