aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2014-08-05STM: new "par:" goal selector, like "all:" but in parallelEnrico Tassi
2014-08-03Fixing #3483 (graceful failing with notations to non-constructors in "match").Hugo Herbelin
2014-07-31Finish fixes on notations and primitive projections, add test-suite files for...Matthieu Sozeau
2014-07-30Add test-suite file for bug #3439.Matthieu Sozeau
2014-07-29Add test-suite file for bug 3454.Matthieu Sozeau
2014-07-29Add test-suite file for bug #3453Matthieu Sozeau
2014-07-24fixup fakeide test-suitePierre Boutillier
2014-07-22Add test-suite file for guard condition on cofixpoints.Maxime Dénès
2014-07-21Fixing output test-suite.Pierre-Marie Pédrot
2014-07-21Adding a test-suite for bug #3422.Pierre-Marie Pédrot
2014-07-16Adding a test-suite for bug #3416.Pierre-Marie Pédrot
2014-07-11Fix Funind test-suite file after patch by Pierre.Matthieu Sozeau
2014-07-09Arith: full integration of the "Numbers" modular frameworkPierre Letouzey
2014-07-03Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanl...Matthieu Sozeau
2014-07-02Indeed simpl never is really honored now.Matthieu Sozeau
2014-06-30Tests for bugs #2834 and #2994.Hugo Herbelin
2014-06-30Completing test for bug report #2830Hugo Herbelin
2014-06-30Synchronized names from the "as" clause with the skeleton of theHugo Herbelin
2014-06-28Quickly fixing bug #2996: typing functions now check when referring toHugo Herbelin
2014-06-26Invalid bug report.Matthieu Sozeau
2014-06-26Fix bug # 3325 using canonical structure declarations where needed.Matthieu Sozeau
2014-06-26Add an option to disable typeclass resolution during conversion, whichMatthieu Sozeau
2014-06-26Merge branch 'tc-test-suite' of https://github.com/JasonGross/coq into JasonG...Matthieu Sozeau
2014-06-26Fixed bug with new semantics of change.Matthieu Sozeau
2014-06-26DuplicateMatthieu Sozeau
2014-06-26This has been fixed.Matthieu Sozeau
2014-06-26Properly refresh the local hintdb database in case an external tactic changedMatthieu Sozeau
2014-06-26Fix test-suite file, adding the proper Fail.Matthieu Sozeau
2014-06-26Bug #3329 is closed.Matthieu Sozeau
2014-06-263392 is now closed thanks to E. Tassi.Matthieu Sozeau
2014-06-26Merge branch 'more-test-suite' of https://github.com/JasonGross/coq into Jaso...Matthieu Sozeau
2014-06-26Fix test-suite files.Matthieu Sozeau
2014-06-26Bug #3301 is closed, the projection cannot be defined anymore.Matthieu Sozeau
2014-06-26Fix test-suite file for opened bug #1596Matthieu Sozeau
2014-06-26Fix test-suite file for bug # 3036, the unification has _never_ succeeded,Matthieu Sozeau
2014-06-26Change interface of refresh universes to get a pbty argument instead ofMatthieu Sozeau
2014-06-26Add an Unset Standard...Matthieu Sozeau
2014-06-24Update some bugs about typeclass resolutionJason Gross
2014-06-23Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344)Enrico Tassi
2014-06-23Fix for bug 1951, allowing at least fully-applied inductives types to be usedMatthieu Sozeau
2014-06-23Fix test-suite script for subst working with let-ins, the following proof was...Matthieu Sozeau
2014-06-23Changed syntax of explicit universes.Matthieu Sozeau
2014-06-23Fix semantics of change p with c to typecheck c at each specific occurrence o...Matthieu Sozeau
2014-06-23Proper handling of the polymorphism flag for Context, fixing HoTT bug #98.Matthieu Sozeau
2014-06-23The uses of the funext axiom forced levels to Set, relaxing its use doesn't.Matthieu Sozeau
2014-06-23The test-suite file couldn't typecheck as it rightly introduces a universe in...Matthieu Sozeau
2014-06-23Fix test-suite script for HoTT coq bug #34Matthieu Sozeau
2014-06-22More test-suite casesJason Gross
2014-06-21- Add an option to refresh only algebraic universes, for e_type_of. The goalMatthieu Sozeau
2014-06-20Fixed bug 3332.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 08:41:54 +0000