aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Expand)AuthorAge
* 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
* Synchronized names from the "as" clause with the skeleton of theGravatar Hugo Herbelin2014-06-30
* Fix test-suite script for subst working with let-ins, the following proof was...Gravatar Matthieu Sozeau2014-06-23
* Changed syntax of explicit universes.Gravatar Matthieu Sozeau2014-06-23
* Fix canonical structure resolution in unification (bug found in Ssreflect).Gravatar Matthieu Sozeau2014-06-08
* - Better parsing and printing of named universes: Type{ident} and foo@{(ident...Gravatar Matthieu Sozeau2014-06-04
* - Force every universe level to be >= Prop, so one cannot "go under" it anymore.Gravatar Matthieu Sozeau2014-06-04
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
* More on injection over a projectable "existT". - Fixing syntax "injection ......Gravatar Hugo Herbelin2014-05-31
* Fixing introduction patterns * and ** when used in a branch so that they do n...Gravatar Hugo Herbelin2014-05-31
* - Fix in kernel conversion not folding the universe constraintsGravatar Matthieu Sozeau2014-05-26
* Simplification and improvement of "subst x" in such a way that itGravatar Hugo Herbelin2014-05-08
* Comment in Funind.v test-suite fileGravatar Matthieu Sozeau2014-05-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-14 15:58:24 +0000