| Commit message (Expand) | Author | Age |
|---|
| * | Update hash of cic.mli in checker/values.ml, |  Matthieu Sozeau | 2015-01-13 |
| * | Update headers. |  Maxime Dénès | 2015-01-12 |
| * | Declarations.mli refactoring: module_type_body = module_body |  Pierre Letouzey | 2015-01-11 |
| * | 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 | 2015-01-06 |
| * | coqchk: flush the pp buffer from time to time | Enrico Tassi | 2014-12-26 |
| * | Vi2vo: fix handling of univ constraints coming from the body | Enrico Tassi | 2014-12-23 |
| * | 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-19 |
| * | 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-18 |
| * | 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-12-17 |
| * | Exit with code 129 when an anomaly occurs. |  Xavier Clerc | 2014-11-14 |
| * | A patch for printing "match" when constructors are defined with let-in |  Hugo Herbelin | 2014-10-20 |
| * | 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-06 |
| * | 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-09-05 |
| * | "allows to", like "allowing to", is improper |  Jason Gross | 2014-08-25 |
| * | Port last changes of the guard condition to checker. | Maxime Dénès | 2014-08-06 |
| * | STM: encapsulate Pp.message in Feedback.feedback |  Carst Tankink | 2014-08-04 |
| * | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin | 2014-08-01 |
| * | Porting guard fix to checker. | Maxime Dénès | 2014-07-22 |
| * | Cleanup substitution inside universe instances, only done through subst_fn now, | Matthieu Sozeau | 2014-07-21 |
| * | all coqide specific files moved into ide/ | Enrico Tassi | 2014-06-25 |
| * | 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-10 |
| * | 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-07 |
| * | - Force every universe level to be >= Prop, so one cannot "go under" it anymore. |  Matthieu Sozeau | 2014-06-04 |
| * | Adapt the checker to polymorphic universes and projections (untested). | Matthieu Sozeau | 2014-05-08 |
| * | - 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-05-06 |
| * | Completing 5eb53b5bc8d765ed75e965f43f1084e18efc8790 (I unfortunately | Hugo Herbelin | 2014-04-29 |
Matthieu Sozeau
Maxime Dénès
Pierre Letouzey
Enrico Tassi
Bruno Barras
Pierre-Marie Pédrot
Xavier Clerc
Hugo Herbelin
Jason Gross
Carst Tankink
Matthieu Sozeau