| Commit message (Expand) | Author | Age |
* | Add appropriate Fail(s) to opened bugs | Jason Gross | 2014-05-10 |
* | Move opened bugs to bugs/opened | Jason Gross | 2014-05-10 |
* | Add more regression tests for univ poly/prim proj | Jason Gross | 2014-05-10 |
* | Code cleaning & factorizing functions in Equality. | Pierre-Marie Pédrot | 2014-05-09 |
* | Update and start testing rewrite-in-type code. | Matthieu Sozeau | 2014-05-09 |
* | More documentation of new features in CHANGE. | Pierre-Marie Pédrot | 2014-05-09 |
* | Refresh universes for Ltac's type_of, as the term can be used anywhere, | Matthieu Sozeau | 2014-05-09 |
* | Merge branch 'working-polyproj-tests' of https://github.com/JasonGross/coq in... | Matthieu Sozeau | 2014-05-09 |
|\ |
|
* | | Fix second-order matching to properly check that the predicate found by | Matthieu Sozeau | 2014-05-09 |
* | | Restore implicit arguments of irreflexivity (fixes bug #3305). | Matthieu Sozeau | 2014-05-09 |
* | | Reuse universe level substitutions for template polymorphism, fixing performance | Matthieu Sozeau | 2014-05-09 |
* | | 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-08 |
* | | Removing comment outdated since eta holds in conversion rule (this | Hugo Herbelin | 2014-05-07 |
* | | 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 |