aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Update test-suite files.Gravatar Matthieu Sozeau2014-09-24
* Fix bug #3656.Gravatar Matthieu Sozeau2014-09-23
* Move the specific map_constr_with_binders_left_to_rightGravatar Matthieu Sozeau2014-09-19
* Fixing #3641 (loop in e_contextually, introduced in r16525).Gravatar Hugo Herbelin2014-09-19
* Fix constrMatching as well as change/e_contextually to allowGravatar Matthieu Sozeau2014-09-18
* Fix debug printing with primitive projections.Gravatar Matthieu Sozeau2014-09-18
* Reductionops: (Co)Fixpoints are always refolded during iotaGravatar Pierre Boutillier2014-09-18
* Fix bug #3593, making constr_eq and progress work up toGravatar Matthieu Sozeau2014-09-17
* Fix bug #3633 properly, by delaying the interpetation of constrs inGravatar Matthieu Sozeau2014-09-17
* Revert "While resolving typeclass evars in clenv, touch only the ones that ap...Gravatar Matthieu Sozeau2014-09-17
* While resolving typeclass evars in clenv, touch only the ones that appear in theGravatar Matthieu Sozeau2014-09-17
* 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
* Undo prints only if coqtop || emacsGravatar Enrico Tassi2014-09-16
* 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
* Fixing printing of @eq which was apparently wrong bug fixed by MS on Wed 10.Gravatar Hugo Herbelin2014-09-15
* Fixing line break in test for #3559.Gravatar Hugo Herbelin2014-09-15
* Avoid backtracking in typeclass search if a solution for a closedGravatar Matthieu Sozeau2014-09-15
* Rework typeclass resolution and control of backtracking.Gravatar Matthieu Sozeau2014-09-15
* Fixing injection bug #3616 on sigma-types.Gravatar Hugo Herbelin2014-09-13
* While we don't have a clean alternative to Clenvtac, add a primitiveGravatar Matthieu Sozeau2014-09-12
* An old typo which was preventing example #3537 to work the same as itGravatar Hugo Herbelin2014-09-12
* Fix test-suite files, and move some opened to closed.Gravatar Matthieu Sozeau2014-09-11
* Other bugs with "inversion as" (collision between user-provided names and gen...Gravatar Hugo Herbelin2014-09-11
* Fix bug #3594: eta for constructors and functions at the same time whichGravatar Matthieu Sozeau2014-09-11
* Fix bug #3596, wrong treatment of projections in compute_constelim_direct.Gravatar Matthieu Sozeau2014-09-11
* Fix bug #3505.Gravatar Matthieu Sozeau2014-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
* Removing dead code relative to the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
* Test for "inversion as" naming bug.Gravatar Hugo Herbelin2014-09-07
* Regression test #3557Gravatar Hugo Herbelin2014-09-07
* Regression test for bug #2883.Gravatar Hugo Herbelin2014-09-07
* Fix bug #3584, elaborating pattern-matching on primitive records to theGravatar Matthieu Sozeau2014-09-06
* 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
* Status error for bug #3459.Gravatar Pierre-Marie Pédrot2014-09-04
* Test for bug #3459.Gravatar Pierre-Marie Pédrot2014-09-04
* Fix bug #3561, correct folding of env in context[] matching.Gravatar Matthieu Sozeau2014-09-04
* Fix bug #3559, ensuring a canonical order of universe level quantifications whenGravatar Matthieu Sozeau2014-09-04
* Add test-suite file for Case derivation on primitive records.Gravatar Matthieu Sozeau2014-09-04
* Add test suite files for closed bugs.Gravatar Matthieu Sozeau2014-09-04
* Fix bug #3563, making syntactic matching of primitive projectionsGravatar Matthieu Sozeau2014-09-04
* Yes another remaining clearing bug with 'apply in'.Gravatar Hugo Herbelin2014-09-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 17:24:46 +0000