| Age | Commit message (Expand) | Author |
|---|
| 2018-01-18 | Merge PR #6448: Cleanup and add debug printers a bit | Maxime Dénès |
| 2017-12-27 | [API] remove large file containing duplicate interfaces | Enrico Tassi |
| 2017-12-22 | Cleanup debug printers a bit, add generated mli. | Gaëtan Gilbert |
| 2017-12-20 | Separate vernac controls and regular commands. | Maxime Dénès |
| 2017-12-17 | [vernac] Split `command.ml` into separate files. | Emilio Jesus Gallego Arias |
| 2017-11-21 | Merge PR #6185: [parser] Remove unnecessary statically initialized hook. | Maxime Dénès |
| 2017-11-19 | [parser] Remove unnecessary statically initialized hook. | Emilio Jesus Gallego Arias |
| 2017-11-15 | [dev] Remove deprecation warning from `base_include` | Emilio Jesus Gallego Arias |
| 2017-10-28 | [toplevel] Export the last document seen after `Drop`. | Emilio Jesus Gallego Arias |
| 2017-07-27 | [api] Fix base_include LTAC parts. | Emilio Jesus Gallego Arias |
| 2017-07-16 | Adapting to 91df40272 (body_of_constant_body moved to global). | Hugo Herbelin |
| 2017-06-16 | Fix a bug in cumulativity | Amin Timany |
| 2017-06-16 | A short cleanup | Amin Timany |
| 2017-06-16 | Clean up universes of constants and inductives | Amin Timany |
| 2017-06-15 | fix dev/base_include (thanks Zimmi48) | Pierre Letouzey |
| 2017-06-07 | Put all plugins behind an "API". | Matej Kosik |
| 2017-04-07 | Fixes for Drop. to work (decl_mode removal and toplevel -> vernac) | Matthieu Sozeau |
| 2017-02-23 | Fixing #use"include" after vernac is added and ltac is moved to a plugin. | Hugo Herbelin |
| 2016-09-14 | Moving Ltac-specific parsing API to ltac/ folder. | Pierre-Marie Pédrot |
| 2016-07-03 | rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError... | Pierre Letouzey |
| 2016-03-21 | Creating a dedicated ltac/ folder for Hightactics. | Pierre-Marie Pédrot |
| 2015-10-30 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-29 | Fixing another instance of bug #3267 in eauto, this time in the | Hugo Herbelin |
| 2015-05-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-04-21 | Fixing #4198 (looking for subterms also in the return clause of match). | Hugo Herbelin |
| 2015-02-27 | Adding a new folder corresponding to the low-level part of the pretyper | Pierre-Marie Pédrot |
| 2014-12-07 | Removing import of Proofview in debugger because its module Goal hides | Hugo Herbelin |
| 2014-10-31 | More "open" by default for trace debugging. | Hugo Herbelin |
| 2014-10-15 | Fix ill-typed debugging function | Matthieu Sozeau |
| 2014-10-10 | Add debug printers for projections, fix printing of evar constraints | Matthieu Sozeau |
| 2014-09-18 | Fix debug printing with primitive projections. | Matthieu Sozeau |
| 2014-09-12 | Fix base_include due to change in argument order of env and evar_map | Matthieu Sozeau |
| 2014-06-28 | More open in base_include | Hugo Herbelin |
| 2014-05-26 | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau |
| 2014-05-06 | Remove Lemmas from base_include, it's not linked in dev/printers anymore | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-01 | Updated debugging printers | Hugo Herbelin |
| 2014-02-24 | app_node, stack, state printers | Pierre Boutillier |
| 2014-01-11 | 'Pretty' printer for wf_paths | Pierre |
| 2014-01-08 | Fix base_include: Toplevel-->Coqloop, Constrintern.intern_constr without evd | Pierre Letouzey |
| 2013-11-25 | Remove the Hiddentac module. | Arnaud Spiwack |
| 2013-11-02 | Removes Refine from the dev tools now that the module has been deleted. | aspiwack |
| 2013-03-21 | Robust display of NotConvertibleTypeField errors (fix #3008, #2995) | letouzey |
| 2013-02-27 | Update debug code according to reorganization into modules. | msozeau |
| 2013-02-27 | Adapt dev/base_include to new Declarations | letouzey |
| 2013-02-21 | Added Evarsolve to the list of modules to open for debugging. | herbelin |
| 2012-10-16 | Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp | letouzey |
| 2012-05-29 | place all pretty-printing files in new dir printing/ | letouzey |
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |
| 2012-05-29 | Strongly reduce the dependencies of grammar.cma, modulo two hacks | letouzey |
