| Age | Commit message (Expand) | Author |
|---|
| 2014-11-08 | Compatibility with 8.4 in the heuristic used to build the induction | Hugo Herbelin |
| 2014-11-06 | Restoring clear_flag (thanks a lot to jonikelee to notice it). | Hugo Herbelin |
| 2014-11-06 | Optimizing when to clear generalized hypotheses in destruct. | Hugo Herbelin |
| 2014-11-06 | Removing "destruct" test not yet working. | Hugo Herbelin |
| 2014-11-03 | Subtle swap of lines to preserve VarInstance src field before checking | Hugo Herbelin |
| 2014-11-03 | Fix to 844431761 on improving elimination with indices, getting rid of | Hugo Herbelin |
| 2014-11-02 | Improving elimination with indices, getting rid of intrusive residual | Hugo Herbelin |
| 2014-11-02 | Some reorganization of the code for destruct/induction: | Hugo Herbelin |
| 2014-11-02 | Fixing file destruct.v. | Hugo Herbelin |
| 2014-10-31 | Enlarge the cases where the like first selection is used in destruct. | Hugo Herbelin |
| 2014-10-31 | Listing a few examples of destruct showing unsatisfactory behaviors. | Hugo Herbelin |
| 2014-10-31 | Avoid "destruct H" to apply on H itself when H is a section variable. | Hugo Herbelin |
| 2014-10-27 | Making destruct on idents with maximal implicit arguments working, by | Hugo Herbelin |
| 2014-10-27 | Ensuring compatibility when an hypothesis used for destruct is | Hugo Herbelin |
| 2014-10-27 | Fixing clash in test destruct.v. | Hugo Herbelin |
| 2014-10-26 | Fixing destruct/induction with a using clause on a non-inductive type, | Hugo Herbelin |
| 2014-10-25 | This commit introduces changes in induction and destruct. | Hugo Herbelin |
| 2014-10-22 | Fixing an evar leak in pattern-matching compilation (#3758). | Hugo Herbelin |
| 2014-10-20 | Fixing a bug in the presence of let-in in inductive arity. | Hugo Herbelin |
| 2014-10-16 | Relaxing again the test on types of replacements in tactic change | Hugo Herbelin |
| 2014-10-13 | Added support for several impossible cases in compilation of "match". | Hugo Herbelin |
| 2014-10-05 | A few improvements on pattern-matching compilation. | Hugo Herbelin |
| 2014-09-30 | Seeing IntroWildcard as an action intro pattern rather than as a naming pattern | Hugo Herbelin |
| 2014-09-29 | Restoring non-uniform delta on local and global constants in 2nd order | Hugo Herbelin |
| 2014-09-29 | Fix test-suite files | Matthieu Sozeau |
| 2014-09-27 | Keyed unification option, compiling the whole standard library | Matthieu Sozeau |
| 2014-09-27 | First version of keyed subterm selection in unification. | Matthieu Sozeau |
| 2014-09-19 | Fixing #3641 (loop in e_contextually, introduced in r16525). | Hugo Herbelin |
| 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 | 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-11 | Other bugs with "inversion as" (collision between user-provided names and gen... | Hugo Herbelin |
| 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 | Parsing of Type@{max(i,j)}. | 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 | Add test-suite file for Case derivation on primitive records. | Matthieu Sozeau |
| 2014-09-03 | Yes another remaining clearing bug with 'apply in'. | Hugo Herbelin |
| 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 |
| 2014-09-02 | An apply test. | Hugo Herbelin |
| 2014-08-30 | Simplify even further the declaration of primitive projections, | Matthieu Sozeau |
| 2014-08-29 | Not using a "cut" in descend_in_conjunctions induced more success. We | Hugo Herbelin |
| 2014-08-28 | Fixing an unnatural selection of subterms larger than expected in the | Hugo Herbelin |
