aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
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
2013-04-17Using Parameter instead of Variable in test-suite/outputherbelin
2013-03-30Continuation of r16346 on filtering local definitions. Refinedherbelin
2013-02-25Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...pboutill
2013-02-17Added propagation of evars unification failure reasons for betterherbelin
2013-02-17Revised the Ltac trace mechanism so that trace breaking due toherbelin
2013-01-18Unset Asymmetric Patternspboutill
2012-12-18Fixing parsing of specific primitive tokens used as notations for patternsherbelin
2012-12-04Revised the strategy for automatic insertion of spaces when printingherbelin
2012-11-17Update output/Search.out after hint-related extra defs in Peanoletouzey
2012-07-21Fixing bug #2835 (the rationale for printing notations was notherbelin
2012-07-06Minor fixes in the test-suite after my recent commitsletouzey
2012-06-14Constrextern is allow to use partially applied notationspboutill
2012-06-12Fixing test-suite after last storm in Pp.pboutill
2012-05-15Notations are back in the "in" clause of pattern matching.pboutill
2012-04-06Fixing a few bugs (see #2571) related to interpretation of multiple bindersherbelin
2012-03-20Fixing alpha-conversion bug #2723 introduced in r12485-12486.herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 10:55:38 +0000