| Commit message (Expand) | Author | Age |
|---|
| ... | |
| * | - 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-10 |
| * | Flattening Level module structure in Univ. |  Pierre-Marie Pédrot | 2014-06-09 |
| * | Function in Univ uselessly exported. | Pierre-Marie Pédrot | 2014-06-08 |
| * | Make kernel reduction code parametric over the handling of universes, | Matthieu Sozeau | 2014-06-06 |
| * | 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-05 |
| * | - 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-04 |
| * | - Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed some | Matthieu Sozeau | 2014-05-28 |
| * | - 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-26 |
| * | Another try at close_proof that should behave better w.r.t. exception handling. | Matthieu Sozeau | 2014-05-16 |
| * | Rewritten the sorting algorithm for universes with a better complexity. | Pierre-Marie Pédrot | 2014-05-13 |
| * | Find a more efficient fix for dealing with template universes: | Matthieu Sozeau | 2014-05-06 |
| * | - Fix bug preventing apply from unfolding Fixpoints. | 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 |
| * | 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 | 2014-05-06 |
| * | Better hashconsing of levels and universes, working with modules. | Matthieu Sozeau | 2014-05-06 |
| * | Be defensive in univ/eq_instances, raise an anomaly on incompatible instances. | Matthieu Sozeau | 2014-05-06 |
| * | Reinstate hashconsing of instances, faster globally. | Matthieu Sozeau | 2014-05-06 |
| * | Restore reasonable performance by not allocating during universe checks, | Matthieu Sozeau | 2014-05-06 |
| * | - Rename eq to equal in Univ, document new modules, set interfaces. | Matthieu Sozeau | 2014-05-06 |
| * | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
| * | Correct handling of hashconsing of constraint sets. The previous implementation | Pierre-Marie Pédrot | 2014-03-05 |
| * | Fixing Pervasives.equality in extraction. | Pierre-Marie Pédrot | 2014-03-03 |
| * | remoteCounter: backup/restore |  Enrico Tassi | 2014-02-26 |
| * | univ: removing dead code | Enrico Tassi | 2014-02-26 |
| * | Optimizing universes: tail-rec, allocation friendly [compare_leq]. |  ppedrot | 2013-10-29 |
| * | More monomorphic List.mem + List.assoc + ... |  letouzey | 2013-10-24 |
| * | Specializing hash functions for widely used types. | ppedrot | 2013-10-24 |
| * | cList: set-as-list functions are now with an explicit comparison | letouzey | 2013-10-23 |
| * | Fix comment for new string syntax (OCaml trunk). |  xclerc | 2013-10-04 |
| * | Removing a bunch of generic equalities. | ppedrot | 2013-09-27 |
| * | Universe counters on slaves are in sync with master |  gareuselesinge | 2013-08-20 |
| * | A version of Univ.check_eq with no anomaly for Evd.set_eq_sort | letouzey | 2013-03-12 |
| * | More monomorphization. | ppedrot | 2013-03-05 |
| * | avoid (Int.equal (cmp ...) 0) when a boolean equality exists | letouzey | 2013-02-19 |
| * | Dir_path --> DirPath | letouzey | 2013-02-19 |
| * | Minor code cleanups, especially take advantage of Dir_path.is_empty | letouzey | 2013-02-18 |
| * | Uniformization of the "anomaly" command. | ppedrot | 2013-01-28 |
| * | Modulification of dir_path | ppedrot | 2012-12-14 |
Matthieu Sozeau
Pierre-Marie Pédrot
Enrico Tassi
ppedrot
letouzey
xclerc
gareuselesinge