| Commit message (Expand) | Author | Age |
|---|
| * | "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 |
| * | Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to | Hugo Herbelin | 2014-04-28 |
| * | Fix guard condition for nested cofixpoints in checker. | Maxime Dénès | 2014-04-10 |
| * | printer for coqchk | Enrico Tassi | 2014-04-08 |
| * | Fixing coqchk. It was my fault, I misused canonical and user equalities | Pierre-Marie Pédrot | 2014-04-04 |
| * | 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-18 |
| * | vi2vo: universes handling finally fixed | Enrico Tassi | 2014-03-11 |
| * | 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-03-05 |
| * | 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-02-26 |
| * | Fixing checker compilation, which was broken by the following commit: | Pierre-Marie Pédrot | 2014-01-19 |
| * | Relaxing the sort elimination check to allow for let-bindings in arities. | Maxime Dénès | 2014-01-18 |
| * | Christmas is over... | Maxime Dénès | 2014-01-15 |
| * | .vi files: .vo files without proofs | Enrico Tassi | 2014-01-04 |
| * | More monomorphic List.mem + List.assoc + ... |  letouzey | 2013-10-24 |
| * | inductive.ml : get rid of some obvious (Lazy.force (lazy t)) | letouzey | 2013-10-24 |
| * | Rtree : cleanup of the comparing code | letouzey | 2013-10-24 |
| * | Get rid of polymorphic equality in "checker/subtyping.ml". |  xclerc | 2013-10-24 |
| * | Turn many List.assoc into List.assoc_f | letouzey | 2013-10-24 |
| * | cList.index is now cList.index_f, same for index0 | letouzey | 2013-10-23 |
| * | Future: ported to Ephemeron + exception enhancing |  gareuselesinge | 2013-10-18 |
| * | Ephemeron: marshaling friendly keys | gareuselesinge | 2013-10-18 |
| * | Getting rid of the use of deprecated elements (from the OCaml standard library). | xclerc | 2013-10-14 |
Jason Gross
Maxime Dénès
Carst Tankink
Hugo Herbelin
Matthieu Sozeau
Enrico Tassi
Pierre-Marie Pédrot
Matthieu Sozeau
Pierre Letouzey
letouzey
xclerc
gareuselesinge