aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2014-10-02Added make dependency in %.out in output tests.Hugo Herbelin
2014-10-02Revert "test-suite: New names for vars but the expected invariant is preserved"Hugo Herbelin
2014-10-02Adapting output/Arguments_renaming.out after fixing printing ofHugo Herbelin
2014-10-01Updating to the new use of 3 universes, after Hurkens is simplified.Hugo Herbelin
2014-10-01Removing test for bug #2080.Pierre-Marie Pédrot
2014-09-30Add a bunch of reproduction files for closed bugs.Xavier Clerc
2014-09-30Add a bunch of reproduction files for bugs.Xavier Clerc
2014-09-30Seeing IntroWildcard as an action intro pattern rather than as a naming patternHugo Herbelin
2014-09-29Restoring non-uniform delta on local and global constants in 2nd orderHugo Herbelin
2014-09-29Adding a test for bug #2428.Pierre-Marie Pédrot
2014-09-29Bug fixed.Matthieu Sozeau
2014-09-29Fix test-suite filesMatthieu Sozeau
2014-09-29In evarconv and unification, expand folded primitive projections toMatthieu Sozeau
2014-09-27Keyed unification option, compiling the whole standard libraryMatthieu Sozeau
2014-09-27First version of keyed subterm selection in unification.Matthieu Sozeau
2014-09-27Fix test-suite file.Matthieu Sozeau
2014-09-27Fix bug #3664 by refolding projections that don't reduce in cbn.Matthieu Sozeau
2014-09-27Fix semantics of matching with folded/unfolded projections to definitelyMatthieu Sozeau
2014-09-27Fix bug #3672, application of primitive projections as coercions.Matthieu Sozeau
2014-09-27Fix bug 3662 by actually reducing primitive projections in cbv/compute.Matthieu Sozeau
2014-09-27Bug fixed.Matthieu Sozeau
2014-09-27Make pattern_of_constr typed so that we can infer the proper patternsMatthieu Sozeau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-27Adapting to naming of evars.Hugo Herbelin
2014-09-26Fix canonical structure resolution which was launched on the results ofMatthieu Sozeau
2014-09-26Add a bunch of reproduction files for bugs.Xavier Clerc
2014-09-26Add missing "Fail" to bug cases.Xavier Clerc
2014-09-26Bug #3566 is fixed.Xavier Clerc
2014-09-26Adding a test for bug #3653.Pierre-Marie Pédrot
2014-09-26Test cases for closed bugs.Xavier Clerc
2014-09-25Add several reproduction files for bugs.Xavier Clerc
2014-09-24Update test-suite files.Matthieu Sozeau
2014-09-23Fix bug #3656.Matthieu Sozeau
2014-09-19Move the specific map_constr_with_binders_left_to_rightMatthieu Sozeau
2014-09-19Fixing #3641 (loop in e_contextually, introduced in r16525).Hugo Herbelin
2014-09-18Fix constrMatching as well as change/e_contextually to allowMatthieu Sozeau
2014-09-18Fix debug printing with primitive projections.Matthieu Sozeau
2014-09-18Reductionops: (Co)Fixpoints are always refolded during iotaPierre Boutillier
2014-09-17Fix bug #3593, making constr_eq and progress work up toMatthieu Sozeau
2014-09-17Fix bug #3633 properly, by delaying the interpetation of constrs inMatthieu Sozeau
2014-09-17Revert "While resolving typeclass evars in clenv, touch only the ones that ap...Matthieu Sozeau
2014-09-17While resolving typeclass evars in clenv, touch only the ones that appear in theMatthieu Sozeau
2014-09-17Update test-suite files after last commit. Add a file for rewrite_stratMatthieu Sozeau
2014-09-17Revert specific syntax for primitive projections, avoiding uglyMatthieu Sozeau
2014-09-16Undo prints only if coqtop || emacsEnrico Tassi
2014-09-16fix test-suite/success/decl_mode.vEnrico Tassi
2014-09-15Add a "Hint Mode ref (+ | -)*" hint for setting a global modeMatthieu Sozeau
2014-09-15Adapting ltac output test to new interpretation of binders.Hugo Herbelin
2014-09-15Fixing printing of @eq which was apparently wrong bug fixed by MS on Wed 10.Hugo Herbelin
2014-09-15Fixing line break in test for #3559.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-13 16:17:28 +0000