| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2012-04-12 | lib directory is cut in 2 cma. | pboutill |
| 2012-04-06 | Removing Dhyp from debugger. | herbelin |
| 2012-03-14 | Everything compiles again. | msozeau |
| 2012-02-01 | Debugger vs tracer: Two different behaviors wrt printing: The debugger | herbelin |
| 2011-10-15 | dev/base_include: display a nice message at the end of the load | letouzey |
| 2011-04-26 | dev/base_include: no more mod_self_id | letouzey |
| 2011-04-13 | - Remove create_evar_defs | msozeau |
| 2011-04-06 | Fix dev/base_include after change of constant_body | letouzey |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-12-23 | Change of nomenclature: rawconstr -> glob_constr | glondu |
| 2010-06-18 | Quick fix for having clenv debug printer working in trunk. | herbelin |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2009-11-09 | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin |
| 2009-11-08 | Fixed "Scheme Equality" when another instance of the scheme on the | herbelin |
| 2009-11-08 | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin |
| 2009-08-07 | Fixed incorrect optimization in Prettyp.pr_located_qualid introduced | herbelin |
| 2009-04-25 | - Fixing #2090 (occur check missing when trying to solve evar-evar equation). | herbelin |
| 2009-01-19 | - Structuring Numbers and fixing Setoid in stdlib's doc. | herbelin |
| 2008-09-02 | Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about | herbelin |
