| Commit message (Expand) | Author | Age |
|---|
| ... | |
| * | Implement module subtyping for polymorphic constants (errors on |  Matthieu Sozeau | 2014-10-02 |
| * | Clean a bit of univ.ml, add credits. | Matthieu Sozeau | 2014-09-18 |
| * | Fix checker treatment of inductives using subst_instances instead of subst_un... | Matthieu Sozeau | 2014-09-05 |
| * | Fix bug #3559, ensuring a canonical order of universe level quantifications when | Matthieu Sozeau | 2014-09-04 |
| * | Simplify even further the declaration of primitive projections, | Matthieu Sozeau | 2014-08-30 |
| * | Fix pretty-printing of the graph in Print Sorted Universes. Type.0 was larger... |  Matthieu Sozeau | 2014-08-18 |
| * | Adding a primitive to merge ContextSets which is more efficient when one |  Pierre-Marie Pédrot | 2014-08-09 |
| * | Cleaning up interface of ContextSet. | Pierre-Marie Pédrot | 2014-08-09 |
| * | Fixing semantics of Univ.Level.equal. | Pierre-Marie Pédrot | 2014-08-04 |
| * | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau | 2014-08-03 |
| * | Useless export of Instance.eqeq. We hashcons everything before calling this | Pierre-Marie Pédrot | 2014-07-31 |
| * | Avoid hconsing instances during appends and conversions from/to arrays. | Matthieu Sozeau | 2014-07-30 |
| * | Universe level maps use HMaps. | Pierre-Marie Pédrot | 2014-07-21 |
| * | Cleanup substitution inside universe instances, only done through subst_fn now, | Matthieu Sozeau | 2014-07-21 |
| * | Cleanup code related to the constraint solving, which sits now outside the | Matthieu Sozeau | 2014-07-03 |
| * | Properly compute the transitive closure of the system of constraints | Matthieu Sozeau | 2014-07-03 |
| * | Add toplevel commands to declare global universes and constraints. | Matthieu Sozeau | 2014-07-01 |
| * | Fix type_of_inductive_knowing_conclusion, relying on an actually broken univ_... | Matthieu Sozeau | 2014-06-25 |
| * | Code factorization in LMap. | Pierre-Marie Pédrot | 2014-06-18 |
| * | Code cleaning in Univ. | Pierre-Marie Pédrot | 2014-06-12 |
| * | In generalized rewrite, avoid retyping completely and constantly the conclusi... | Matthieu Sozeau | 2014-06-11 |
| * | 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-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 |
Matthieu Sozeau
Matthieu Sozeau
Pierre-Marie Pédrot