| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2014-06-10 | Removing dead code in checker/univ.ml. | Pierre-Marie Pédrot |
| 2014-06-10 | Removing explanations of universe inconsistencies from the checker. They | Pierre-Marie Pédrot |
| 2014-06-10 | Providing the checker with its own version of the Univ file. | Pierre-Marie Pédrot |
| 2014-06-07 | Removing 'open Univ' from checker. | Pierre-Marie Pédrot |
| 2014-06-07 | Moving a Thread.yield in check_interrupt. | Pierre-Marie Pédrot |
| 2014-06-07 | Adding a new Control file centralizing the control options of Coq. | Pierre-Marie Pédrot |
| 2014-06-04 | - Force every universe level to be >= Prop, so one cannot "go under" it anymore. | Matthieu Sozeau |
| 2014-05-08 | Adapt the checker to polymorphic universes and projections (untested). | Matthieu Sozeau |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 2014-05-06 | - Fix comparison of universes. | Matthieu Sozeau |
| 2014-05-06 | - Rename eq to equal in Univ, document new modules, set interfaces. | Matthieu Sozeau |
| 2014-05-06 | Correct rebase on STM code. Thanks to E. Tassi for help on dealing with | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-29 | Completing 5eb53b5bc8d765ed75e965f43f1084e18efc8790 (I unfortunately | Hugo Herbelin |
| 2014-04-28 | Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to | Hugo Herbelin |
| 2014-04-10 | Fix guard condition for nested cofixpoints in checker. | Maxime Dénès |
| 2014-04-08 | printer for coqchk | Enrico Tassi |
| 2014-04-04 | Fixing coqchk. It was my fault, I misused canonical and user equalities | Pierre-Marie Pédrot |
| 2014-03-18 | Printing backtraces in coqchk while in debug mode. | Pierre-Marie Pédrot |
| 2014-03-18 | Fixing checker with respect to new kernel name structure and hashmaps. | Pierre-Marie Pédrot |
| 2014-03-11 | vi2vo: universes handling finally fixed | Enrico Tassi |
| 2014-03-05 | Adding a canary library. This canary is imperfect. It allows serialization | Pierre-Marie Pédrot |
| 2014-03-05 | Added a new module HMap. It works (almost) like Map, except that it expects | Pierre-Marie Pédrot |
| 2014-03-05 | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey |
| 2014-03-05 | Adding a CSet module in Coq lib. | Pierre-Marie Pédrot |
| 2014-02-26 | checker and votour ported to new vo format (after -vi2vo) | Enrico Tassi |
| 2014-02-26 | votour: better error messages | Enrico Tassi |
| 2014-02-26 | checker: less useless error messages | Enrico Tassi |
| 2014-02-26 | fix checker w.r.t. mutual_inductive_body and constant_body | Enrico Tassi |
| 2014-02-26 | fix checker w.r.t. Dyn.t validation | Enrico Tassi |
| 2014-01-19 | Fixing checker compilation, which was broken by the following commit: | Pierre-Marie Pédrot |
| 2014-01-18 | Relaxing the sort elimination check to allow for let-bindings in arities. | Maxime Dénès |
| 2014-01-15 | Christmas is over... | Maxime Dénès |
| 2014-01-04 | .vi files: .vo files without proofs | Enrico Tassi |
