| Age | Commit message (Expand) | Author |
|---|
| 2014-11-25 | Adapting to current semantics of "simpl non-evaluable-cst" | Hugo Herbelin |
| 2014-11-25 | Experimenting using unification when matching evar/meta free subterms | Hugo Herbelin |
| 2014-11-22 | Add test-suite file for dependent rewriting example by Vadim Zaliva and | Matthieu Sozeau |
| 2014-11-18 | Fixing a little bug with nested but convertible occurrences in "destruct at". | Hugo Herbelin |
| 2014-11-18 | Fixing detection of occurrences in the presence of nested subterms for | Hugo Herbelin |
| 2014-11-16 | Enforcing a stronger difference between the two syntaxes "simpl | Hugo Herbelin |
| 2014-11-16 | Fixing side bug in db37c9f3f32ae7 delaying interpretation of the | Hugo Herbelin |
| 2014-11-14 | Preserving the good effect of 014e5ac92a on not leaving dangling local | Hugo Herbelin |
| 2014-11-13 | Removing yet another source of remaining local definitions. | Hugo Herbelin |
| 2014-11-08 | Follow up to experimental eager evar unification in bcba6d1bc9: | Hugo Herbelin |
| 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 |
