| Age | Commit message (Expand) | Author |
|---|
| 2014-06-10 | Fixing Sorting Universes in a world where le and lt constraints may be | Pierre-Marie Pédrot |
| 2014-06-10 | Compute the trace of a universe inconsistency only when explicitly required | Pierre-Marie Pédrot |
| 2014-06-10 | Made explanations for universe inconsistencies optional. They are only used | Pierre-Marie Pédrot |
| 2014-06-10 | Specialize the type of [Univ.compare_neq] so that it is clear it is only used | Pierre-Marie Pédrot |
| 2014-06-10 | Imperatively check touched universes in compare_neq functions. This ensures | Pierre-Marie Pédrot |
| 2014-06-10 | - Fix substitution of universes which needlessly hashconsed existing universes. | Matthieu Sozeau |
| 2014-06-10 | Oops, one refactoring was not compiled. | Matthieu Sozeau |
| 2014-06-10 | More cleanup/reorganizing of univ.ml to separate constraint/universe handling... | Matthieu Sozeau |
| 2014-06-10 | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau |
| 2014-06-10 | Remove unused function in univ | Matthieu Sozeau |
| 2014-06-09 | Flattening Level module structure in Univ. | Pierre-Marie Pédrot |
| 2014-06-08 | ind_tables: always declare side effects (Closes: HOTT#110) | Enrico Tassi |
| 2014-06-08 | Function in Univ uselessly exported. | 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-06 | Make kernel reduction code parametric over the handling of universes, | Matthieu Sozeau |
| 2014-06-05 | Dedicated map module for type universes. It uses hashmaps, which are | Pierre-Marie Pédrot |
| 2014-06-05 | Removing dead code from Univ. | Pierre-Marie Pédrot |
| 2014-06-04 | - Force every universe level to be >= Prop, so one cannot "go under" it anymore. | Matthieu Sozeau |
| 2014-06-04 | - Fix hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau |
| 2014-06-02 | Fixing incorrect printf format. | Pierre-Marie Pédrot |
| 2014-05-28 | - Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed some | Matthieu Sozeau |
| 2014-05-26 | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau |
| 2014-05-26 | Update infer_conv to record trivial Prop <= Type i constraints that are neede... | Matthieu Sozeau |
| 2014-05-22 | Fix native_compute for systems with a limited size for the command line. | Guillaume Melquiond |
| 2014-05-16 | Revert "Decent error message when a constant is not found" | Enrico Tassi |
| 2014-05-16 | Decent error message when a constant is not found | Enrico Tassi |
| 2014-05-16 | Another try at close_proof that should behave better w.r.t. exception handling. | Matthieu Sozeau |
| 2014-05-13 | Rewritten the sorting algorithm for universes with a better complexity. | Pierre-Marie Pédrot |
| 2014-05-11 | Using Maps to handle imports in Safe_typing. The order is irrelevant indeed, | Pierre-Marie Pédrot |
| 2014-05-09 | Reuse universe level substitutions for template polymorphism, fixing performance | Matthieu Sozeau |
| 2014-05-08 | Avoid allocations in type_of_inductive | Matthieu Sozeau |
| 2014-05-08 | Fast-path equality of sorts in compare_constr* | Matthieu Sozeau |
| 2014-05-06 | Add missing case for primitive projection in fold_map. | Matthieu Sozeau |
| 2014-05-06 | Fix extraction taking a type in the wrong environment. | Matthieu Sozeau |
| 2014-05-06 | Find a more efficient fix for dealing with template universes: | Matthieu Sozeau |
| 2014-05-06 | Add doc on the new API for universe polymorphism and primitive projections | Matthieu Sozeau |
| 2014-05-06 | - Fix eq_constr_universes restricted to Sorts.equal | 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 | Adapt Y. Bertot's path on private inductives (now the keyword is "Private"). | Yves Bertot |
| 2014-05-06 | - Fix handling of polymorphic inductive elimination schemes. | Matthieu Sozeau |
| 2014-05-06 | Cleanup in constr, correct classification of polymorphic defs. | Matthieu Sozeau |
| 2014-05-06 | - Fix index-list to show computational relations for rewriting files. | Matthieu Sozeau |
| 2014-05-06 | Various fixes of universe polymorphism and projections when they're set. | Matthieu Sozeau |
| 2014-05-06 | - Fix Check to use the constraints inferred during type inference. | Matthieu Sozeau |
| 2014-05-06 | Improve universe/level comparison using hashes. | Matthieu Sozeau |
| 2014-05-06 | In kernel/univ.ml, better allocation behavior, better eq_univs function | Matthieu Sozeau |
| 2014-05-06 | Compat with ocaml 3.12 | Matthieu Sozeau |
| 2014-05-06 | - Fix comparison of universes. | Matthieu Sozeau |
