aboutsummaryrefslogtreecommitdiff
path: root/dev/top_printers.ml
AgeCommit message (Expand)Author
2014-12-30Compatibility ocaml 3.12.Hugo Herbelin
2014-12-16More printers for ltac signatures.Hugo Herbelin
2014-12-04Reactivating option "Set Printing Existential Instances" for asking printing ...Hugo Herbelin
2014-10-13Adding printers for ppproofview.Hugo Herbelin
2014-10-10Add debug printers for projections, fix printing of evar constraintsMatthieu Sozeau
2014-10-09Adding printer for named_context_val and Goal.goal in debugger.Hugo Herbelin
2014-10-07Adding a printer for hints.Hugo Herbelin
2014-10-02Fixing interpretation of constr under binders which was broken afterHugo Herbelin
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-18Fix debug printing with primitive projections.Matthieu Sozeau
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-09-10VernacExtend does not dispatch on type anymore.Pierre-Marie Pédrot
2014-08-26Debug RAKAMPierre Boutillier
2014-06-11- Fix bug #3368, due to wrong use of the Cst_stack for projections.Matthieu Sozeau
2014-06-10Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Matthieu Sozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:32:19 +0000