| Commit message (Expand) | Author | Age |
|---|
| * | First version of keyed subterm selection in unification. |  Matthieu Sozeau | 2014-09-27 |
| * | Fix test-suite file. | Matthieu Sozeau | 2014-09-27 |
| * | Fix bug #3664 by refolding projections that don't reduce in cbn. | Matthieu Sozeau | 2014-09-27 |
| * | Fix semantics of matching with folded/unfolded projections to definitely | Matthieu Sozeau | 2014-09-27 |
| * | Fix bug #3672, application of primitive projections as coercions. | Matthieu Sozeau | 2014-09-27 |
| * | Fix bug 3662 by actually reducing primitive projections in cbv/compute. | Matthieu Sozeau | 2014-09-27 |
| * | Bug fixed. | Matthieu Sozeau | 2014-09-27 |
| * | Make pattern_of_constr typed so that we can infer the proper patterns | Matthieu Sozeau | 2014-09-27 |
| * | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau | 2014-09-27 |
| * | Adapting to naming of evars. |  Hugo Herbelin | 2014-09-27 |
| * | Fix canonical structure resolution which was launched on the results of | Matthieu Sozeau | 2014-09-26 |
| * | Add a bunch of reproduction files for bugs. |  Xavier Clerc | 2014-09-26 |
| * | Add missing "Fail" to bug cases. | Xavier Clerc | 2014-09-26 |
| * | Bug #3566 is fixed. | Xavier Clerc | 2014-09-26 |
| * | Adding a test for bug #3653. |  Pierre-Marie Pédrot | 2014-09-26 |
| * | Test cases for closed bugs. | Xavier Clerc | 2014-09-26 |
| * | Add several reproduction files for bugs. | Xavier Clerc | 2014-09-25 |
| * | Update test-suite files. | Matthieu Sozeau | 2014-09-24 |
| * | Fix bug #3656. | Matthieu Sozeau | 2014-09-23 |
| * | Move the specific map_constr_with_binders_left_to_right | Matthieu Sozeau | 2014-09-19 |
| * | Fixing #3641 (loop in e_contextually, introduced in r16525). | Hugo Herbelin | 2014-09-19 |
| * | 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-18 |
| * | 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-17 |
| * | Undo prints only if coqtop || emacs |  Enrico Tassi | 2014-09-16 |
| * | fix test-suite/success/decl_mode.v | Enrico Tassi | 2014-09-16 |
| * | 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-15 |
| * | Fixing injection bug #3616 on sigma-types. | Hugo Herbelin | 2014-09-13 |
| * | 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-12 |
| * | 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-11 |
| * | 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-10 |
| * | - Fix printing and parsing of primitive projections, including the Set | Matthieu Sozeau | 2014-09-09 |
Matthieu Sozeau
Hugo Herbelin
Xavier Clerc
Pierre-Marie Pédrot
Pierre Boutillier
Enrico Tassi