| Commit message (Expand) | Author | Age |
|---|
| * | Fix a pervasive equality use. |  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 |
| * | Add doc on the new API for universe polymorphism and primitive projections | Matthieu Sozeau | 2014-05-06 |
| * | Fix derive plugin to properly treat universes | Matthieu Sozeau | 2014-05-06 |
| * | Keep track of universes on coercion applications even if they're not polymorp... | Matthieu Sozeau | 2014-05-06 |
| * | Comment in Funind.v test-suite file | Matthieu Sozeau | 2014-05-06 |
| * | Proper calculation of constructor levels, forgetting the level of lets. | Matthieu Sozeau | 2014-05-06 |
| * | Refresh some universes in cases.ml as they might appear in the term. | Matthieu Sozeau | 2014-05-06 |
| * | Correct universe handling in program coercions (bug #2378). | Matthieu Sozeau | 2014-05-06 |
| * | Fix set_leq_sort refusing max(u,Set) <= Set when u is flexible. | Matthieu Sozeau | 2014-05-06 |
| * | Retype application of fix_proto to get the right universes in Program | 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 declarations of monomorphic assumptions | Matthieu Sozeau | 2014-05-06 |
| * | Allow records whose sort is defined by a constant. | Matthieu Sozeau | 2014-05-06 |
| * | - Fix RecTutorial, and mutual induction schemes getting the wrong names. | Matthieu Sozeau | 2014-05-06 |
| * | Fix program Fixpoint not taking care of universes. | Matthieu Sozeau | 2014-05-06 |
| * | - Fixes for canonical structure resolution (check that the initial term indee... | Matthieu Sozeau | 2014-05-06 |
| * | Fix restrict_universe_context to not remove useful constraints. | Matthieu Sozeau | 2014-05-06 |
| * | - Fix eq_constr_universes restricted to Sorts.equal | Matthieu Sozeau | 2014-05-06 |
| * | Remove postponed constraints (unused) | Matthieu Sozeau | 2014-05-06 |
| * | Fixes after rebase. The use of pf_constr_of_global is problematic in presence... | 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 |
| * | Honor the Opaque flag for projections in simpl. | Matthieu Sozeau | 2014-05-06 |
| * | In case two constants/vars/rels are _not_ defined, force unification of unive... | Matthieu Sozeau | 2014-05-06 |
| * | Fix context forgetting universes (temporary, the fix is not exactly right). | 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 |
| * | 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 |
| * | Fix printing of projections with implicits. | Matthieu Sozeau | 2014-05-06 |
| * | Fix inversion of notations for projections. | 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 | 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 |
| * | 'Pretty' printer for wf_paths |  Pierre | 2014-05-06 |
| * | md5 for MacOS | Pierre | 2014-05-06 |
| * | Lemmas: export standard proof terminator |  Enrico Tassi | 2014-05-06 |
Matthieu Sozeau
Yves Bertot
Pierre
Enrico Tassi