aboutsummaryrefslogtreecommitdiff
path: root/dev/top_printers.ml
AgeCommit message (Expand)Author
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-30Getting rid of Pp.msgppedrot
2012-05-29Split Egrammar into Egramml and Egramcoqletouzey
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-03-02Noise for nothingpboutill
2012-02-01Debugger vs tracer: Two different behaviors wrt printing: The debuggerherbelin
2011-10-17Revert "New evar_map printer ppevmfull which can typically be installed for"herbelin
2011-10-17New evar_map printer ppevmfull which can typically be installed forherbelin
2011-09-25Polishing commits r14492, r14448 and r14407 (tactics propagateherbelin
2011-08-04Fix unification: detect invalid evar instantiations due to scoping earlier.msozeau
2011-07-16Finally, pr_goal seems to work for printing v8.2 style goal in debugger.herbelin
2011-06-21Cleaning debugging printer relative to new proof engine. Inherbelin
2011-05-13A new mechanism to handle errors.aspiwack
2011-02-07Factorize code of rewrite to make way for a new implementation using themsozeau
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2010-11-08Print universes in debugging printersglondu
2010-11-07Delayed the evar normalization in error messages to the last minuteherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-23Names: remove obsolete mod_self_idletouzey
2010-06-18Quick fix for having clenv debug printer working in trunk.herbelin
2010-06-12Fixing spelling: pr_coma -> pr_commaherbelin
2010-06-12Added debugging printer for the idmap used at evar definition time forherbelin
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
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