| Age | Commit message (Expand) | Author |
|---|
| 2014-05-08 | Fixing test-suite for bug #3043. | Pierre-Marie Pédrot |
| 2014-05-08 | Fixing output test-suite: since universe polymorphism, the Print command | Pierre-Marie Pédrot |
| 2014-05-08 | Code cleaning in Tacinterp: factorizing some uses of tclEVARS. | Pierre-Marie Pédrot |
| 2014-05-07 | Removing comment outdated since eta holds in conversion rule (this | Hugo Herbelin |
| 2014-05-06 | Adding test-suite for bug #3242. | Pierre-Marie Pédrot |
| 2014-05-06 | 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 |
