aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/set_raw_db
Commit message (Collapse)AuthorAge
* Allègement de l'affichage des références par le printer si possibleGravatar herbelin2007-01-22
(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