aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Expand)AuthorAge
* Improving evar restriction (this is a risky change, as I remember aGravatar Hugo Herbelin2014-12-07
* Take benefit of improved name preservation of evars in e2fa65fcc.Gravatar Hugo Herbelin2014-12-04
* When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' ifGravatar Hugo Herbelin2014-12-02
* Adapting to current semantics of "simpl non-evaluable-cst"Gravatar Hugo Herbelin2014-11-25
* Experimenting using unification when matching evar/meta free subtermsGravatar Hugo Herbelin2014-11-25
* Add test-suite file for dependent rewriting example by Vadim Zaliva andGravatar Matthieu Sozeau2014-11-22
* Fixing a little bug with nested but convertible occurrences in "destruct at".Gravatar Hugo Herbelin2014-11-18
* Fixing detection of occurrences in the presence of nested subterms forGravatar Hugo Herbelin2014-11-18
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
* Fixing side bug in db37c9f3f32ae7 delaying interpretation of theGravatar Hugo Herbelin2014-11-16
* Preserving the good effect of 014e5ac92a on not leaving dangling localGravatar Hugo Herbelin2014-11-14
* Removing yet another source of remaining local definitions.Gravatar Hugo Herbelin2014-11-13
* Follow up to experimental eager evar unification in bcba6d1bc9:Gravatar Hugo Herbelin2014-11-08
* Compatibility with 8.4 in the heuristic used to build the inductionGravatar Hugo Herbelin2014-11-08
* Restoring clear_flag (thanks a lot to jonikelee to notice it).Gravatar Hugo Herbelin2014-11-06
* Optimizing when to clear generalized hypotheses in destruct.Gravatar Hugo Herbelin2014-11-06
* Removing "destruct" test not yet working.Gravatar Hugo Herbelin2014-11-06
* Subtle swap of lines to preserve VarInstance src field before checkingGravatar Hugo Herbelin2014-11-03
* Fix to 844431761 on improving elimination with indices, getting rid ofGravatar Hugo Herbelin2014-11-03
* Improving elimination with indices, getting rid of intrusive residualGravatar Hugo Herbelin2014-11-02
* Some reorganization of the code for destruct/induction:Gravatar Hugo Herbelin2014-11-02
* Fixing file destruct.v.Gravatar Hugo Herbelin2014-11-02
* Enlarge the cases where the like first selection is used in destruct.Gravatar Hugo Herbelin2014-10-31
* Listing a few examples of destruct showing unsatisfactory behaviors.Gravatar Hugo Herbelin2014-10-31
* Avoid "destruct H" to apply on H itself when H is a section variable.Gravatar Hugo Herbelin2014-10-31
* Making destruct on idents with maximal implicit arguments working, byGravatar Hugo Herbelin2014-10-27
* Ensuring compatibility when an hypothesis used for destruct isGravatar Hugo Herbelin2014-10-27
* Fixing clash in test destruct.v.Gravatar Hugo Herbelin2014-10-27
* Fixing destruct/induction with a using clause on a non-inductive type,Gravatar Hugo Herbelin2014-10-26
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Fixing an evar leak in pattern-matching compilation (#3758).Gravatar Hugo Herbelin2014-10-22
* Fixing a bug in the presence of let-in in inductive arity.Gravatar Hugo Herbelin2014-10-20
* Relaxing again the test on types of replacements in tactic changeGravatar Hugo Herbelin2014-10-16
* Added support for several impossible cases in compilation of "match".Gravatar Hugo Herbelin2014-10-13
* A few improvements on pattern-matching compilation.Gravatar Hugo Herbelin2014-10-05
* Seeing IntroWildcard as an action intro pattern rather than as a naming patternGravatar Hugo Herbelin2014-09-30
* Restoring non-uniform delta on local and global constants in 2nd orderGravatar Hugo Herbelin2014-09-29
* Fix test-suite filesGravatar Matthieu Sozeau2014-09-29
* Keyed unification option, compiling the whole standard libraryGravatar Matthieu Sozeau2014-09-27
* First version of keyed subterm selection in unification.Gravatar Matthieu Sozeau2014-09-27
* Fixing #3641 (loop in e_contextually, introduced in r16525).Gravatar Hugo Herbelin2014-09-19
* Update test-suite files after last commit. Add a file for rewrite_stratGravatar Matthieu Sozeau2014-09-17
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* fix test-suite/success/decl_mode.vGravatar Enrico Tassi2014-09-16
* Add a "Hint Mode ref (+ | -)*" hint for setting a global modeGravatar Matthieu Sozeau2014-09-15
* Adapting ltac output test to new interpretation of binders.Gravatar Hugo Herbelin2014-09-15
* Other bugs with "inversion as" (collision between user-provided names and gen...Gravatar Hugo Herbelin2014-09-11
* Parsing and printing of primitive projections, fix buggy behavior whenGravatar Matthieu Sozeau2014-09-10
* Fixing inversion after having fixed intros_replacingGravatar Hugo Herbelin2014-09-10
* Example for apply and evars.Gravatar Hugo Herbelin2014-09-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 02:54:12 +0000