aboutsummaryrefslogtreecommitdiff
path: root/dev/top_printers.ml
AgeCommit message (Expand)Author
2016-05-10Removing the Entry module now that rules need not be marshalled.Pierre-Marie Pédrot
2016-05-04Moving the Val module to Geninterp.Pierre-Marie Pédrot
2016-04-08Fixing printing of toplevel values.Pierre-Marie Pédrot
2016-03-19Do not export entry_key from Pcoq anymore.Pierre-Marie Pédrot
2016-03-19Simplifying the code of Entry.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-14Removing constr generic argument.Pierre-Marie Pédrot
2016-01-02Simplification of grammar_prod_item type.Pierre-Marie Pédrot
2015-12-21Finer-grained types for toplevel values.Pierre-Marie Pédrot
2015-12-21Using dynamic values in tactic evaluation.Pierre-Marie Pédrot
2015-12-18Tying the loop in tactic printing API.Pierre-Marie Pédrot
2015-10-27Type-safe Egramml.grammar_prod_item.Pierre-Marie Pédrot
2015-10-26Pcoq entries are given a proper module.Pierre-Marie Pédrot
2015-10-14Reverting modifications in dev/top_printers pushed mistakenly.Pierre-Marie Pédrot
2015-10-14Fixing perfomance issue of auto hints induced by universes.Pierre-Marie Pédrot
2015-10-06Splitting kernel universe code in two modules.Pierre-Marie Pédrot
2015-09-20Better debug printers for module paths.Maxime Dénès
2015-07-30A printer for printing constants of the env (maybe useful when there are not ...Hugo Herbelin
2015-02-19Adding a possible DEPRECATED flag to VERNAC EXTEND statements.Pierre-Marie Pédrot
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 05:37:36 +0000