| Age | Commit message (Expand) | Author |
|---|
| 2014-05-11 | Eliminating a potentially quadratic behaviour in Require, by using maps | Pierre-Marie Pédrot |
| 2014-05-06 | Fix extraction taking a type in the wrong environment. | Matthieu Sozeau |
| 2014-05-06 | Avoid u+k <= v constraints, don't take the sup of an algebraic universe during | Matthieu Sozeau |
| 2014-05-06 | - Add back some compatibility functions to avoid rewriting plugins. | Matthieu Sozeau |
| 2014-05-06 | - Fix arity handling in retyping (de Bruijn bug!) | Matthieu Sozeau |
| 2014-05-06 | Fix restrict_universe_context removing some universes that do appear in the t... | Matthieu Sozeau |
| 2014-05-06 | Fix restrict_universe_context to not remove useful constraints. | Matthieu Sozeau |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 2014-05-06 | Adapt universe polymorphic branch to new handling of futures for delayed proofs. | Matthieu Sozeau |
| 2014-05-06 | Fix issue #88: restrict_universe_context was wrongly forgetting about constra... | Matthieu Sozeau |
| 2014-05-06 | Adapt Y. Bertot's path on private inductives (now the keyword is "Private"). | Yves Bertot |
| 2014-05-06 | - Fix abstract forgetting about new constraints. | Matthieu Sozeau |
| 2014-05-06 | - Fix handling of polymorphic inductive elimination schemes. | Matthieu Sozeau |
| 2014-05-06 | Fix printing of projections with implicits. | 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 | Fix interface for template polymorphism, cleaning up code in all typing algor... | Matthieu Sozeau |
| 2014-05-06 | Initial work on reintroducing old-style polymorphism for compatibility (the s... | Matthieu Sozeau |
| 2014-05-06 | Correct rebase on STM code. Thanks to E. Tassi for help on dealing with | Matthieu Sozeau |
| 2014-05-06 | Rework handling of universes on top of the STM, allowing for delayed | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-05-01 | Fixing ml-doc. | Pierre-Marie Pédrot |
| 2014-04-29 | Native compiler: hide compiled files in a .coq-native subdirectory. | Maxime Dénès |
| 2014-04-25 | Fixing various backtrace recordings. | Pierre-Marie Pédrot |
| 2014-04-23 | Removing dead code, thanks to new OCaml warnings and a bit of scripting. | Pierre-Marie Pédrot |
| 2014-04-08 | Add an option -Q (tentative name). | Guillaume Melquiond |
| 2014-04-02 | Fix Bug 3217 | Pierre Boutillier |
| 2014-03-20 | Missing equalities in Names-like structures. | Pierre-Marie Pédrot |
| 2014-03-18 | STM: make -async-proofs on work from coqc too | Enrico Tassi |
| 2014-03-14 | Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it had | Pierre-Marie Pédrot |
| 2014-03-11 | vi2vo: universes handling finally fixed | Enrico Tassi |
| 2014-03-08 | Using HMaps in global references. | Pierre-Marie Pédrot |
| 2014-03-07 | Fix lookup of native files when option -R is missing. | Guillaume Melquiond |
| 2014-03-05 | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey |
| 2014-03-03 | Goptions do not rely anymore on generic equality. | Pierre-Marie Pédrot |
| 2014-03-01 | Fixing pervasive comparisons | Pierre-Marie Pédrot |
| 2014-02-28 | Fixing a Pervasive.compare. | Pierre-Marie Pédrot |
| 2014-02-26 | Library: when compiling multiple files, reset the opaque tables | Enrico Tassi |
| 2014-02-26 | Lazyconstr -> Opaqueproof | Enrico Tassi |
| 2014-02-26 | New compilation mode -vi2vo | Enrico Tassi |
| 2014-02-03 | Allocation-friendly mapping functions in Nametab. | Pierre-Marie Pédrot |
| 2014-01-05 | STM: modules do not prevent proofs from being ASync | Enrico Tassi |
| 2014-01-05 | coqtop: -check-vi-tasks and -schedule-vi-checking | Enrico Tassi |
| 2014-01-04 | .vi files: .vo files without proofs | Enrico Tassi |
| 2013-12-24 | Qed: feedback when type checking is done | Enrico Tassi |
| 2013-12-12 | Patch for supporting [From Xxx Require Yyy Zzz.] | Gregory Malecha |
| 2013-12-02 | Print logical name rather than path (thus allowing reproducible tests). | xclerc |
| 2013-11-24 | Better implementation of summary unfreezing. | Pierre-Marie Pédrot |
| 2013-11-22 | Using hashes in Summary, like the previous commit did with Dyn. | Pierre-Marie Pédrot |
| 2013-11-22 | Using hashes instead of strings in dynamic tags. In case of collision, an | Pierre-Marie Pédrot |
