| Age | Commit message (Expand) | Author |
|---|
| 2014-09-19 | Fixing #3641 (loop in e_contextually, introduced in r16525). | Hugo Herbelin |
| 2014-09-18 | Fix constrMatching as well as change/e_contextually to allow | Matthieu Sozeau |
| 2014-09-18 | Fix debug printing with primitive projections. | Matthieu Sozeau |
| 2014-09-18 | Reductionops: (Co)Fixpoints are always refolded during iota | Pierre Boutillier |
| 2014-09-17 | Fix bug #3593, making constr_eq and progress work up to | Matthieu Sozeau |
| 2014-09-17 | Fix bug #3633 properly, by delaying the interpetation of constrs in | Matthieu Sozeau |
| 2014-09-17 | Revert "While resolving typeclass evars in clenv, touch only the ones that ap... | Matthieu Sozeau |
| 2014-09-17 | While resolving typeclass evars in clenv, touch only the ones that appear in the | Matthieu Sozeau |
| 2014-09-17 | Update test-suite files after last commit. Add a file for rewrite_strat | Matthieu Sozeau |
| 2014-09-17 | Revert specific syntax for primitive projections, avoiding ugly | Matthieu Sozeau |
| 2014-09-16 | Undo prints only if coqtop || emacs | Enrico Tassi |
| 2014-09-16 | fix test-suite/success/decl_mode.v | Enrico Tassi |
| 2014-09-15 | Add a "Hint Mode ref (+ | -)*" hint for setting a global mode | Matthieu Sozeau |
| 2014-09-15 | Adapting ltac output test to new interpretation of binders. | Hugo Herbelin |
| 2014-09-15 | Fixing printing of @eq which was apparently wrong bug fixed by MS on Wed 10. | Hugo Herbelin |
| 2014-09-15 | Fixing line break in test for #3559. | Hugo Herbelin |
| 2014-09-15 | Avoid backtracking in typeclass search if a solution for a closed | Matthieu Sozeau |
| 2014-09-15 | Rework typeclass resolution and control of backtracking. | Matthieu Sozeau |
| 2014-09-13 | Fixing injection bug #3616 on sigma-types. | Hugo Herbelin |
| 2014-09-12 | While we don't have a clean alternative to Clenvtac, add a primitive | Matthieu Sozeau |
| 2014-09-12 | An old typo which was preventing example #3537 to work the same as it | Hugo Herbelin |
| 2014-09-11 | Fix test-suite files, and move some opened to closed. | Matthieu Sozeau |
| 2014-09-11 | Other bugs with "inversion as" (collision between user-provided names and gen... | Hugo Herbelin |
| 2014-09-11 | Fix bug #3594: eta for constructors and functions at the same time which | Matthieu Sozeau |
| 2014-09-11 | Fix bug #3596, wrong treatment of projections in compute_constelim_direct. | Matthieu Sozeau |
| 2014-09-11 | Fix bug #3505. | Matthieu Sozeau |
| 2014-09-10 | Parsing and printing of primitive projections, fix buggy behavior when | Matthieu Sozeau |
| 2014-09-10 | Fixing inversion after having fixed intros_replacing | Hugo Herbelin |
| 2014-09-10 | Example for apply and evars. | Hugo Herbelin |
| 2014-09-09 | - Fix printing and parsing of primitive projections, including the Set | Matthieu Sozeau |
| 2014-09-08 | Fixing TestRefine test-suite file. | Pierre-Marie Pédrot |
| 2014-09-08 | Removing dead code relative to the XML plugin. | Pierre-Marie Pédrot |
| 2014-09-08 | Parsing of Type@{max(i,j)}. | Matthieu Sozeau |
| 2014-09-07 | Test for "inversion as" naming bug. | Hugo Herbelin |
| 2014-09-07 | Regression test #3557 | Hugo Herbelin |
| 2014-09-07 | Regression test for bug #2883. | Hugo Herbelin |
| 2014-09-06 | Fix bug #3584, elaborating pattern-matching on primitive records to the | Matthieu Sozeau |
| 2014-09-06 | Fix checker to handle projections with eta and universe polymorphism correctly. | Matthieu Sozeau |
| 2014-09-05 | Fix primitive projections declarations for inductive records. | Matthieu Sozeau |
| 2014-09-04 | Status error for bug #3459. | Pierre-Marie Pédrot |
| 2014-09-04 | Test for bug #3459. | Pierre-Marie Pédrot |
| 2014-09-04 | Fix bug #3561, correct folding of env in context[] matching. | Matthieu Sozeau |
| 2014-09-04 | Fix bug #3559, ensuring a canonical order of universe level quantifications when | Matthieu Sozeau |
| 2014-09-04 | Add test-suite file for Case derivation on primitive records. | Matthieu Sozeau |
| 2014-09-04 | Add test suite files for closed bugs. | Matthieu Sozeau |
| 2014-09-04 | Fix bug #3563, making syntactic matching of primitive projections | Matthieu Sozeau |
| 2014-09-03 | Yes another remaining clearing bug with 'apply in'. | Hugo Herbelin |
| 2014-09-03 | Test-suite for bug #2818. | Pierre-Marie Pédrot |
| 2014-09-02 | Adding a test-suite for second-order matching order and indexes. | Pierre-Marie Pédrot |
| 2014-09-02 | Another fix than 19a7a5789c to avoid descend_in_conjunction to use | Hugo Herbelin |
