aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/top_printers.ml
Commit message (Expand)AuthorAge
* Fixing extra returns in top_printers.ml (msg_notice not same semantics as pp).Gravatar Hugo Herbelin2016-07-19
* closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-01
|\
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| * Pfedit.get_current_context refinement (fix #4523)Gravatar Matthieu Sozeau2016-05-26
* | Removing the Entry module now that rules need not be marshalled.Gravatar Pierre-Marie Pédrot2016-05-10
* | Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
* | Fixing printing of toplevel values.Gravatar Pierre-Marie Pédrot2016-04-08
* | Do not export entry_key from Pcoq anymore.Gravatar Pierre-Marie Pédrot2016-03-19
* | Simplifying the code of Entry.Gravatar Pierre-Marie Pédrot2016-03-19
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Removing constr generic argument.Gravatar Pierre-Marie Pédrot2016-01-14
* | Simplification of grammar_prod_item type.Gravatar Pierre-Marie Pédrot2016-01-02
* | Finer-grained types for toplevel values.Gravatar Pierre-Marie Pédrot2015-12-21
* | Using dynamic values in tactic evaluation.Gravatar Pierre-Marie Pédrot2015-12-21
* | Tying the loop in tactic printing API.Gravatar Pierre-Marie Pédrot2015-12-18
* | Type-safe Egramml.grammar_prod_item.Gravatar Pierre-Marie Pédrot2015-10-27
* | Pcoq entries are given a proper module.Gravatar Pierre-Marie Pédrot2015-10-26
| * Reverting modifications in dev/top_printers pushed mistakenly.Gravatar Pierre-Marie Pédrot2015-10-14
| * Fixing perfomance issue of auto hints induced by universes.Gravatar Pierre-Marie Pédrot2015-10-14
* | Splitting kernel universe code in two modules.Gravatar Pierre-Marie Pédrot2015-10-06
* | Better debug printers for module paths.Gravatar Maxime Dénès2015-09-20
|/
* A printer for printing constants of the env (maybe useful when there are not ...Gravatar Hugo Herbelin2015-07-30
* Adding a possible DEPRECATED flag to VERNAC EXTEND statements.Gravatar Pierre-Marie Pédrot2015-02-19
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
* Update headers.Gravatar Maxime Dénès2015-01-12
* Compatibility ocaml 3.12.Gravatar Hugo Herbelin2014-12-30
* More printers for ltac signatures.Gravatar Hugo Herbelin2014-12-16
* Reactivating option "Set Printing Existential Instances" for asking printing ...Gravatar Hugo Herbelin2014-12-04
* Adding printers for ppproofview.Gravatar Hugo Herbelin2014-10-13
* Add debug printers for projections, fix printing of evar constraintsGravatar Matthieu Sozeau2014-10-10
* Adding printer for named_context_val and Goal.goal in debugger.Gravatar Hugo Herbelin2014-10-09
* Adding a printer for hints.Gravatar Hugo Herbelin2014-10-07
* Fixing interpretation of constr under binders which was broken afterGravatar Hugo Herbelin2014-10-02
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Fix debug printing with primitive projections.Gravatar Matthieu Sozeau2014-09-18
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* VernacExtend does not dispatch on type anymore.Gravatar Pierre-Marie Pédrot2014-09-10
* Debug RAKAMGravatar Pierre Boutillier2014-08-26
* - Fix bug #3368, due to wrong use of the Cst_stack for projections.Gravatar Matthieu Sozeau2014-06-11
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Fix issue #88: restrict_universe_context was wrongly forgetting about constra...Gravatar Matthieu Sozeau2014-05-06
* 'Pretty' printer for wf_pathsGravatar Pierre2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Adding a debug printer for futures.Gravatar Pierre-Marie Pédrot2014-04-25
* Better representation of evar filters: we represent the vacuous filters ofGravatar Pierre-Marie Pédrot2014-04-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 16:52:25 +0000