aboutsummaryrefslogtreecommitdiff
path: root/parsing/printmod.ml
AgeCommit message (Expand)Author
2012-05-29place all pretty-printing files in new dir printing/letouzey
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-03-02Noise for nothingpboutill
2011-11-24Added a DEPRECATED flag in declaration of options. For now only two options a...ppedrot
2011-05-21Restore display of notation when printing an inductive such as sigletouzey
2011-05-11Print Module (Type) M now tries to print more detailsletouzey
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2008-10-15Report des commits 11417 et 11437 de la v8.2soubiran
2008-09-05Report 11364 de 8.2 vers trunk (bugs affichage Print Module)herbelin
2008-03-14Ajout des alias de module dans le noyau.soubiran
2008-02-01Beaoucoup de changements dans la representation interne des modules.soubiran
2004-07-16Nouvelle en-têteherbelin
2003-05-08Petite correction d'affichage de modulescoq
2003-04-14Correction bug PR#278coq
2003-01-31Pour satisfaire ProofGeneralcoq
2002-09-20La notation with dependante + affichage dependante de moduels corrigecoq
2002-08-19Pretty-printing preliminaire des modules, commandescoq
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 22:51:19 +0000