| Age | Commit message (Expand) | Author |
|---|
| 2014-05-08 | Encapsulating some clausenv uses. This simplifies the control flow of some | Pierre-Marie Pédrot |
| 2014-05-08 | Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic." | Hugo Herbelin |
| 2014-05-08 | Avoid "revert" to retype-check the goal, and move it to a "new" tactic. | Hugo Herbelin |
| 2014-05-08 | Typo reference manual | Hugo Herbelin |
| 2014-05-08 | Isolating a function "make_abstraction", new name of "letin_abstract", | Hugo Herbelin |
| 2014-05-08 | Simplification and improvement of "subst x" in such a way that it | Hugo Herbelin |
| 2014-05-08 | Renaming new_induct -> induction; new_destruct -> destruct. | Hugo Herbelin |
| 2014-05-08 | Little reorganization of generalize tactics code w/o semantic changes. | Hugo Herbelin |
| 2014-05-08 | 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 | Avoid allocations in type_of_inductive | Matthieu Sozeau |
| 2014-05-08 | Fast-path equality of sorts in compare_constr* | Matthieu Sozeau |
| 2014-05-08 | Adapt the checker to polymorphic universes and projections (untested). | Matthieu Sozeau |
| 2014-05-08 | Moving Dnet-related code to tactics/. | Pierre-Marie Pédrot |
| 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 |
