aboutsummaryrefslogtreecommitdiff
path: root/dev/top_printers.ml
AgeCommit message (Expand)Author
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Fix issue #88: restrict_universe_context was wrongly forgetting about constra...Matthieu Sozeau
2014-05-06'Pretty' printer for wf_pathsPierre
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-25Adding a debug printer for futures.Pierre-Marie Pédrot
2014-04-23Better representation of evar filters: we represent the vacuous filters ofPierre-Marie Pédrot
2014-04-05Printers for ltac environments.Hugo Herbelin
2014-04-02A debug printer for Evd.Filter.tPierre Boutillier
2014-02-26Lazyconstr -> OpaqueproofEnrico Tassi
2014-02-24app_node, stack, state printersPierre Boutillier
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 14:14:26 +0000