| Commit message (Expand) | Author | Age |
|---|
| * | Make kernel reduction code parametric over the handling of universes, |  Matthieu Sozeau | 2014-06-06 |
| * | Collecting in Namegen those conventional default names that are used in diffe... |  Hugo Herbelin | 2014-06-04 |
| * | Fix canonical structure resolution (makes test-suite files go through again). | Matthieu Sozeau | 2014-06-04 |
| * | - Allow parsing of @const@{instance} for specifying universe instances of pol... | Matthieu Sozeau | 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-04 |
| * | - Keep all <= constraints during refinement, otherwise we might miss collapse... | Matthieu Sozeau | 2014-06-04 |
| * | cbn understand ! Arguments directive |  Pierre Boutillier | 2014-06-04 |
| * | Use of "H"-based names for propositional hypotheses obtained by | Hugo Herbelin | 2014-06-01 |
| * | Dead code + typo. | Hugo Herbelin | 2014-05-31 |
| * | - Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed some | Matthieu Sozeau | 2014-05-28 |
| * | Cbn reduces Pos.compare p~1 q~1 to Pos.compare p q | Pierre Boutillier | 2014-05-26 |
| * | Reduction.Stack.Fix/Case stores Cst_stack.t | Pierre Boutillier | 2014-05-26 |
| * | Cst_stack before stack (abstraction leak in whd_gen) | Pierre Boutillier | 2014-05-26 |
| * | cbn: args list instead of arg number | Pierre Boutillier | 2014-05-26 |
| * | Reductionops.Stack.map & Reduction.iterate_whd_gen | Pierre | 2014-05-26 |
| * | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau | 2014-05-26 |
| * | More fixes of unification with primitive projections (missed cases during the... | Matthieu Sozeau | 2014-05-16 |
| * | Fix unification of non-unfoldable primitive projections in evarconv. | Matthieu Sozeau | 2014-05-16 |
| * | Refresh universes for Ltac's type_of, as the term can be used anywhere, | Matthieu Sozeau | 2014-05-09 |
| * | Fix second-order matching to properly check that the predicate found by | Matthieu Sozeau | 2014-05-09 |
| * | Reuse universe level substitutions for template polymorphism, fixing performance | Matthieu Sozeau | 2014-05-09 |
| * | Cleanup code in pretyping/evarutil | Matthieu Sozeau | 2014-05-08 |
| * | Fix performance problem with unification in presence of universes (bug #3302)... | Matthieu Sozeau | 2014-05-08 |
| * | - Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ... | Matthieu Sozeau | 2014-05-08 |
| * | Moving Dnet-related code to tactics/. |  Pierre-Marie Pédrot | 2014-05-08 |
| * | - Fix treatment of global universe constraints which should be passed along | Matthieu Sozeau | 2014-05-06 |
| * | Find a more efficient fix for dealing with template universes: | Matthieu Sozeau | 2014-05-06 |
| * | Try a new way of handling template universe levels | Matthieu Sozeau | 2014-05-06 |
| * | - Add back some compatibility functions to avoid rewriting plugins. | Matthieu Sozeau | 2014-05-06 |
| * | Keep track of universes on coercion applications even if they're not polymorp... | 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 |
| * | - Fix arity handling in retyping (de Bruijn bug!) | Matthieu Sozeau | 2014-05-06 |
| * | Allow records whose sort is defined by a constant. | Matthieu Sozeau | 2014-05-06 |
| * | - Fixes for canonical structure resolution (check that the initial term indee... | 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 |
| * | - 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 |
| * | 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 |
| * | Adapt Y. Bertot's path on private inductives (now the keyword is "Private"). |  Yves Bertot | 2014-05-06 |
| * | - Fix comparison of universes. | 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 |
| * | Fix interface for template polymorphism, cleaning up code in all typing algor... | Matthieu Sozeau | 2014-05-06 |
| * | Properly reinstate old-style polymorphism in the kernel and pretyping/retyping. | Matthieu Sozeau | 2014-05-06 |
| * | Initial work on reintroducing old-style polymorphism for compatibility (the s... | Matthieu Sozeau | 2014-05-06 |
Matthieu Sozeau
Hugo Herbelin
Pierre Boutillier
Pierre-Marie Pédrot
Yves Bertot