aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* 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 clash in output test-suite Cases.Gravatar Hugo Herbelin2014-10-23
* Taking into account factorization of consecutive names of same typesGravatar Hugo Herbelin2014-10-23
* Fixing typo in output test Notations.Gravatar Hugo Herbelin2014-10-22
* Fix test-suite for #2729.Gravatar Maxime Dénès2014-10-22
* Fixing an evar leak in pattern-matching compilation (#3758).Gravatar Hugo Herbelin2014-10-22
* Adapting output tests to the removal of the new token warning and toGravatar Hugo Herbelin2014-10-21
* More precise test for #3459.Gravatar Hugo Herbelin2014-10-21
* Fixing a (new) part of bug #2729.Gravatar Hugo Herbelin2014-10-20
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
* 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
* Fix test-suite scripts.Gravatar Matthieu Sozeau2014-10-16
* Bug fixed by Hugo.Gravatar Matthieu Sozeau2014-10-16
* Adding a timeout to bug #2447.Gravatar Pierre-Marie Pédrot2014-10-15
* To stay closer to non-primitive projections, only unfold primitiveGravatar Matthieu Sozeau2014-10-15
* Fix for bug #3618.Gravatar Matthieu Sozeau2014-10-15
* Closed bug 3710.Gravatar Matthieu Sozeau2014-10-15
* Bug 3692 is fixed.Gravatar Matthieu Sozeau2014-10-15
* Bug 3628 is fixed.Gravatar Matthieu Sozeau2014-10-15
* Fix test-suite files which failed due to usage of $(admit)$ whichGravatar Matthieu Sozeau2014-10-15
* Fix bug 3637.Gravatar Matthieu Sozeau2014-10-15
* Reenable FO unification of primitive projections and their eta-expandedGravatar Matthieu Sozeau2014-10-15
* Fix test-suite file after moving back to using C as the nameGravatar Matthieu Sozeau2014-10-15
* Implement a different strategy to expand primitive projections only whenGravatar Matthieu Sozeau2014-10-15
* Fix bug #3698: stack overflow due to eta+canonical structures inGravatar Matthieu Sozeau2014-10-14
* Added support for several impossible cases in compilation of "match".Gravatar Hugo Herbelin2014-10-13
* Fixing the anomaly in bug #3045 (a filter was not type-safe inGravatar Hugo Herbelin2014-10-08
* Add test-suite file for the projection unfolding bug I just fixed.Gravatar Matthieu Sozeau2014-10-07
* Fix test-suite file 3352 which was containing the wrong test.Gravatar Matthieu Sozeau2014-10-07
* Fix test-suite file to test original bug, not the failure of the guardGravatar Matthieu Sozeau2014-10-07
* A few improvements on pattern-matching compilation.Gravatar Hugo Herbelin2014-10-05
* Classify segfaults as failures in opened bugs.Gravatar Xavier Clerc2014-10-03
* Classify segfaults as failures in opened bugsGravatar Xavier Clerc2014-10-03
* Fixing #3657 (check that both sides of a "change with" have the sameGravatar Hugo Herbelin2014-10-03
* Test for bug #3652 fixed in 0fb36157b9baGravatar Hugo Herbelin2014-10-03
* Fixing #3623 (unbound evars in types in a call to "change with").Gravatar Hugo Herbelin2014-10-03
* Add a bunch of reproduction files for bugs.Gravatar Xavier Clerc2014-10-03
* Adapting output/Arguments_renaming continued.Gravatar Hugo Herbelin2014-10-03
* Implement module subtyping for polymorphic constants (errors onGravatar Matthieu Sozeau2014-10-02
* Fixing bug #2810 (autounfold on local variable declared as hint but cleared).Gravatar Hugo Herbelin2014-10-02
* An evar name changed in output test.Gravatar Hugo Herbelin2014-10-02
* Adapting the output test Notations:Gravatar Hugo Herbelin2014-10-02
* Added make dependency in %.out in output tests.Gravatar Hugo Herbelin2014-10-02
* Revert "test-suite: New names for vars but the expected invariant is preserved"Gravatar Hugo Herbelin2014-10-02
* Adapting output/Arguments_renaming.out after fixing printing ofGravatar Hugo Herbelin2014-10-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 09:36:20 +0000