| Commit message (Expand) | Author | Age |
|---|
| * | Add regression tests for univ. poly. and prim proj |  Jason Gross | 2014-05-06 |
| * | Remove Lemmas from base_include, it's not linked in dev/printers anymore |  Matthieu Sozeau | 2014-05-06 |
| * | Cleanup before merge with the trunk | Matthieu Sozeau | 2014-05-06 |
| * | Use new tactic combinators in tclABSTRACT, to avoid blowup when using V82.tac... | Matthieu Sozeau | 2014-05-06 |
| * | Add missing case for primitive projection in fold_map. | Matthieu Sozeau | 2014-05-06 |
| * | Fix after merge. | Matthieu Sozeau | 2014-05-06 |
| * | Add incompatibilities paragraph in doc about universe polymorphism. | Matthieu Sozeau | 2014-05-06 |
| * | - Fix treatment of global universe constraints which should be passed along | Matthieu Sozeau | 2014-05-06 |
| * | Fix extraction taking a type in the wrong environment. | Matthieu Sozeau | 2014-05-06 |
| * | Fix Field_tac to get fast reification again, with the fix on template univers... | 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 |
| * | Print universes in module printing | Matthieu Sozeau | 2014-05-06 |
| * | Fix funind w.r.t. universes | Matthieu Sozeau | 2014-05-06 |
| * | 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 |
Jason Gross
Matthieu Sozeau
Yves Bertot