aboutsummaryrefslogtreecommitdiff
path: root/dev/top_printers.ml
AgeCommit message (Expand)Author
2009-11-13Remove useless ppevd (which is identical to ppevm)glondu
2009-11-11Promote evar_defs to evar_map (in Evd)glondu
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
2009-08-02Improved parameterization of Coq:herbelin
2009-05-20- Fixing declarative mode in presence of high use of Change_evars nodesherbelin
2009-04-27- Cleaning (unification of ML names, removal of obsolete code,herbelin
2009-02-19On remplace evar_map par evar_defs (seul evar_defs est désormais exporté aspiwack
2008-10-19- Export de pattern_ident vers les ARGUMENT EXTEND and co.herbelin
2008-07-01Various bug fixes in type classes and subtac:msozeau
2008-06-06ajout d'un printer pour les contraintes d'univers + correction d'un bug sur l...soubiran
2008-04-24- Add pretty-printers for Idpred, Cpred and transparent_state, used formsozeau
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2008-04-14Diverses corrections herbelin
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2008-02-08Add printer for Pp.std_ppcmds...msozeau
2007-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
2007-10-03Ajout de eelim, ecase, edestruct et einduction (expérimental).herbelin
2007-08-29- Débogueur: positionnement de set_detype_anonymous pour ne pasherbelin
2007-04-17 Rajout du mot Fix dans le printervsiles
2007-04-17Retablissement de Fix dans print_pure_constr vsiles
2007-01-22Allègement de l'affichage des références par le printer si possibleherbelin
2007-01-19Export de l'afficheur de substitutions de noms de modules pour le débogueurherbelin
2006-09-26mise a jour du nouveau ring et ajout du nouveau field, avant renommagesbarras
2006-09-22Tout petit bug d'affichage dans constr_display (top_printers)herbelin
2006-01-30Plutôt pas de contraction des match dans le déboggueurherbelin
2006-01-29Ajout printer Idset.therbelin
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
2006-01-04Restauration des commandes de débogage PrintConstr et PrintPureConstr (suite...herbelin
2006-01-04Remise en place des commandes vernaculaires PrintConstr et PrintPureConstr (d...herbelin
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...herbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...herbelin
2005-12-02Changement des named_contextgregoire
2005-02-18Ajout constant printerherbelin
2005-01-02Découpage des printers pour ne pas avoir de dépendances en la vm dans les p...herbelin
2004-12-29Ajout printer bigintherbelin
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
2004-11-12Changement dans les boxed values .gregoire
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-09-17restructuration des printers: proofs passe avant parsingbarras
2004-09-15hiding the meta_map in evar_defsbarras
2004-09-08unification encore...barras
2004-07-16Nouvelle en-têteherbelin
2004-03-15Ajout affichage contexte localherbelin
2003-04-16prettyprint des constr_substituted + un wrapping de prglobal pour qu'il n'ech...letouzey
2003-04-07Globalisation tactiquesherbelin
2003-04-07Options d'affichage maintenant dans Constrexternherbelin
2002-12-05Ajout affichage fconstrherbelin
2002-11-14Réforme de l'interprétation des termes :herbelin