aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
2015-10-22Fixing a bug in reporting ill-formed inductive.Hugo Herbelin
2015-10-11Fixing test-suiteHugo Herbelin
2015-10-11Fixing untimely unexpected warning "Collision between bound variables" (#4317).Hugo Herbelin
2015-10-11Refining 0c320e79ba30 in fixing interpretation of constr under bindersHugo Herbelin
2015-09-15Test for bug #4269.Pierre-Marie Pédrot
2015-09-03Update test-suite after 518049fe7.Maxime Dénès
2015-07-27Output test for bug #2169.Pierre-Marie Pédrot
2015-06-24Fix test-suite after 1343b69221ce3eeb3154732e73bbdc0044b224a8.Maxime Dénès
2015-03-09Do not display the status of monomorphic constants unless in universe-polymor...Guillaume Melquiond
2015-03-05Fix testsuite with respect to the new formatting of Fail messages.Guillaume Melquiond
2015-02-15Undo: back to 8.4 semantics (Close #3514)Enrico Tassi
2015-01-12Fixing name of evars in output test Notation.v.Hugo Herbelin
2014-12-15Adapted test file for About.Pierre Courtieu
2014-12-15About now accepts hypothesis names and goal selector.Pierre Courtieu
2014-12-15Tests for Searchxxx commands added and modified.Pierre Courtieu
2014-11-11Adapting output tests to current naming of evars, even if unclearHugo Herbelin
2014-11-06Consequence of changing the definition of Nat.shiftl and Nat.shiftr.Hugo Herbelin
2014-10-23Fixing clash in output test-suite Cases.Hugo Herbelin
2014-10-23Taking into account factorization of consecutive names of same typesHugo Herbelin
2014-10-22Fixing typo in output test Notations.Hugo Herbelin
2014-10-21Adapting output tests to the removal of the new token warning and toHugo Herbelin
2014-10-20A patch for printing "match" when constructors are defined with let-inHugo Herbelin
2014-10-03Adapting output/Arguments_renaming continued.Hugo Herbelin
2014-10-02An evar name changed in output test.Hugo Herbelin
2014-10-02Adapting the output test Notations: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-09-27Adapting to naming of evars.Hugo Herbelin
2014-09-18Reductionops: (Co)Fixpoints are always refolded during iotaPierre Boutillier
2014-09-15Fixing printing of @eq which was apparently wrong bug fixed by MS on Wed 10.Hugo Herbelin
2014-08-25Grammar: "avoiding to" isn't proper, eitherJason Gross
2014-08-12Upgrading output tests.Hugo Herbelin
2014-07-21Fixing output test-suite.Pierre-Marie Pédrot
2014-06-04cbn understand ! Arguments directivePierre Boutillier
2014-05-08Fixing output test-suite: since universe polymorphism, the Print commandPierre-Marie Pédrot
2014-04-28Fixing #3293 (eta-expansion at "match" printing time was failingHugo Herbelin
2014-03-01Never suppress the typing constraint of bound variables whose name wasPierre-Marie Pédrot
2014-02-28test-suite: opaque term -> opaque proofPierre Boutillier
2014-02-28test-suite: New names for vars but the expected invariant is preservedPierre Boutillier
2014-02-28Fix output test-suite 'simpl tactic' -> 'reduction tactics'Pierre Boutillier
2013-12-19test-suite/output/Notations : evar number changePierre Boutillier
2013-12-02Test suite: update output reference.xclerc
2013-12-02Print logical name rather than path (thus allowing reproducible tests).xclerc
2013-11-03test-suite fixuppboutill
2013-10-08Fixing 2 output test-suites.ppedrot
2013-09-03Fixing some tests from the test-suite.ppedrot
2013-08-08Fix testsuite so that it works with STMgareuselesinge
2013-07-29better error message for unexpected renaming (closes #2987)gareuselesinge
2013-05-09Updating some output tests in test-suite:herbelin
2013-04-17Renaming SearchAbout into Search and Search into SearchHead.herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 12:27:00 +0000