aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Expand)AuthorAge
...
* 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
* - Fix printing and parsing of primitive projections, including the SetGravatar Matthieu Sozeau2014-09-09
* Fixing TestRefine test-suite file.Gravatar Pierre-Marie Pédrot2014-09-08
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
* Fix checker to handle projections with eta and universe polymorphism correctly.Gravatar Matthieu Sozeau2014-09-06
* Fix primitive projections declarations for inductive records.Gravatar Matthieu Sozeau2014-09-05
* Add test-suite file for Case derivation on primitive records.Gravatar Matthieu Sozeau2014-09-04
* Yes another remaining clearing bug with 'apply in'.Gravatar Hugo Herbelin2014-09-03
* Adding a test-suite for second-order matching order and indexes.Gravatar Pierre-Marie Pédrot2014-09-02
* Another fix than 19a7a5789c to avoid descend_in_conjunction to useGravatar Hugo Herbelin2014-09-02
* An apply test.Gravatar Hugo Herbelin2014-09-02
* Simplify even further the declaration of primitive projections,Gravatar Matthieu Sozeau2014-08-30
* Not using a "cut" in descend_in_conjunctions induced more success. WeGravatar Hugo Herbelin2014-08-29
* Fixing an unnatural selection of subterms larger than expected in theGravatar Hugo Herbelin2014-08-28
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* instanciation is French, instantiation is EnglishGravatar Jason Gross2014-08-25
* Fixing a bug introduced in the extension of 'apply in' + simplifying code.Gravatar Hugo Herbelin2014-08-25
* Fixing unification of subterms identified by patterns.Gravatar Hugo Herbelin2014-08-18
* A reorganization of the "assert" tactics (hopefully uniform namingGravatar Hugo Herbelin2014-08-18
* Fix test-suite file.Gravatar Matthieu Sozeau2014-08-18
* Fixing too restrictive detection of resolution of evars in "apply in"Gravatar Hugo Herbelin2014-08-16
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
* Fix Funind test-suite file after patch by Pierre.Gravatar Matthieu Sozeau2014-07-11
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 12:21:57 +0000