aboutsummaryrefslogtreecommitdiff
path: root/dev/top_printers.ml
AgeCommit message (Expand)Author
2014-01-11'Pretty' printer for wf_pathsPierre
2013-11-30Adding printing of ltac envs to debugger.Pierre-Marie Pédrot
2013-09-24Adding evar printing to debugger.ppedrot
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-08-04Small cleaning of printing coercion failures in Ltac interpretation.ppedrot
2013-07-05Removing SortArgType.ppedrot
2013-07-05Expurgating the useless difference between List0 and List1 at theppedrot
2013-06-27Getting rid of IntroPatternArgType.ppedrot
2013-06-21Cutting the dependency of Genarg in constr_expr, glob_constrppedrot
2013-06-19Adding genarg printer to debugger.ppedrot
2013-06-18Proof-of-concept: moved four easy-to-handle generic arguments toppedrot
2013-06-12Added Genarg as generic argument type.ppedrot
2013-06-06Uniformizing generic argument types.ppedrot
2013-05-14Removing useless uses of Gmap.ppedrot
2013-03-21Robust display of NotConvertibleTypeField errors (fix #3008, #2995)letouzey
2013-02-26kernel/declarations becomes a pure mliletouzey
2013-02-19Dir_path --> DirPathletouzey
2013-02-18use List.rev_map whenever possibleletouzey
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-12-18Modulification of mod_bound_idppedrot
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
2012-10-06still some more dead code removalletouzey
2012-10-06Clean-up : no more Proof_type.proof_treeletouzey
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-08Updating headers.herbelin
2012-08-05Revert "Fixing include printers"pboutill
2012-08-03Fixing include printersppedrot
2012-07-30Bigint: avoid dependency over Ppletouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 20:59:02 +0000