| Age | Commit message (Expand) | Author |
|---|
| 2015-03-25 | Exporting memory representation of STM tasks for votour. | Pierre-Marie Pédrot |
| 2015-03-24 | Functorized interface over object representation in votour. | Pierre-Marie Pédrot |
| 2015-03-24 | Fixing representation of dynamics in votour (again). | Pierre-Marie Pédrot |
| 2015-03-23 | coqchk: more prints when -debug | Enrico Tassi |
| 2015-03-18 | Fixing internal representation of Dyn.t in votour. | Pierre-Marie Pédrot |
| 2015-03-02 | Now accepting unit props in mutual definitions | Bruno Barras |
| 2015-02-26 | Fix checker after addition of a universe context in with t := c constraints. | Matthieu Sozeau |
| 2015-02-12 | Revert "Using same code for browsing physical directories in coqtop and coqdep." | Hugo Herbelin |
| 2015-02-12 | Revert "Capital letter in plugins." (Sorry, was not intended to be pushed) | Hugo Herbelin |
| 2015-02-12 | Capital letter in plugins. | Hugo Herbelin |
| 2015-02-12 | Using same code for browsing physical directories in coqtop and coqdep. | Hugo Herbelin |
| 2015-02-11 | Fixing bug #4019, and checker blow-up at once. | Pierre-Marie Pédrot |
| 2015-02-11 | Clarifying the implementation of universe hashconsing. | Pierre-Marie Pédrot |
| 2015-02-05 | Windows: open .vo files in binary mode | Enrico Tassi |
| 2015-01-13 | Update hash of cic.mli in checker/values.ml, | Matthieu Sozeau |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2015-01-11 | Declarations.mli refactoring: module_type_body = module_body | Pierre Letouzey |
| 2015-01-06 | Fix checker's treatment of template polymorphic | Matthieu Sozeau |
| 2015-01-06 | rename: vi -> vio | Enrico Tassi |
| 2015-01-06 | updated include file for debugging | Bruno Barras |
| 2015-01-06 | improve efficiency of the reduction interpreter of the checker | Bruno Barras |
| 2014-12-26 | coqchk: flush the pp buffer from time to time | Enrico Tassi |
| 2014-12-23 | Vi2vo: fix handling of univ constraints coming from the body | Enrico Tassi |
| 2014-12-19 | Fixing performance issue of checker validation. | Pierre-Marie Pédrot |
| 2014-12-19 | Fixing checker representation of values. | Pierre-Marie Pédrot |
| 2014-12-19 | update md5 sums to make "make check" work | Enrico Tassi |
| 2014-12-19 | Fix sigsegv in checker | Enrico Tassi |
| 2014-12-18 | Fixing checker representation of universe lists. | Pierre-Marie Pédrot |
| 2014-12-18 | Backporting the change in lists of universes to the checker. | Pierre-Marie Pédrot |
| 2014-12-17 | checker: Change in library on disk values, now using context_sets instead of | Matthieu Sozeau |
| 2014-12-17 | Ensuring the good invariants of hashcons table generation in the API. | Pierre-Marie Pédrot |
| 2014-12-17 | Update checker/values and cic due to changes in case_info and record_body. | Matthieu Sozeau |
| 2014-11-14 | Exit with code 129 when an anomaly occurs. | Xavier Clerc |
| 2014-10-20 | A patch for printing "match" when constructors are defined with let-in | Hugo Herbelin |
| 2014-09-06 | Remove debug printing code | Matthieu Sozeau |
| 2014-09-06 | Cleanup code for looking up projection bodies. | Matthieu Sozeau |
| 2014-09-06 | Fix checker to handle projections with eta and universe polymorphism correctly, | Matthieu Sozeau |
| 2014-09-06 | Fix checker to handle projections with eta and universe polymorphism correctly. | Matthieu Sozeau |
| 2014-09-06 | Fix checking of constants in checker. Prelude can now be checked. | Matthieu Sozeau |
| 2014-09-05 | Remove unused substitution functions in checker. | Matthieu Sozeau |
| 2014-09-05 | Fix checker treatment of inductives using subst_instances instead of subst_un... | Matthieu Sozeau |
| 2014-09-05 | Fix checker/values.ml with latest changes due to projections and universes. | Matthieu Sozeau |
| 2014-09-05 | Rename eta_expand_ind_stacks, fix the one from the checker and adapt | Matthieu Sozeau |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross |
| 2014-08-06 | Port last changes of the guard condition to checker. | Maxime Dénès |
| 2014-08-04 | STM: encapsulate Pp.message in Feedback.feedback | Carst Tankink |
| 2014-08-01 | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin |
| 2014-07-22 | Porting guard fix to checker. | Maxime Dénès |
| 2014-07-21 | Cleanup substitution inside universe instances, only done through subst_fn now, | Matthieu Sozeau |
| 2014-06-25 | all coqide specific files moved into ide/ | Enrico Tassi |
