aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
Commit message (Expand)AuthorAge
* Adapting output tests to current naming of evars, even if unclearGravatar Hugo Herbelin2014-11-11
* Consequence of changing the definition of Nat.shiftl and Nat.shiftr.Gravatar Hugo Herbelin2014-11-06
* Fixing clash in output test-suite Cases.Gravatar Hugo Herbelin2014-10-23
* Taking into account factorization of consecutive names of same typesGravatar Hugo Herbelin2014-10-23
* Fixing typo in output test Notations.Gravatar Hugo Herbelin2014-10-22
* Adapting output tests to the removal of the new token warning and toGravatar Hugo Herbelin2014-10-21
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
* Adapting output/Arguments_renaming continued.Gravatar Hugo Herbelin2014-10-03
* An evar name changed in output test.Gravatar Hugo Herbelin2014-10-02
* Adapting the output test Notations:Gravatar Hugo Herbelin2014-10-02
* Revert "test-suite: New names for vars but the expected invariant is preserved"Gravatar Hugo Herbelin2014-10-02
* Adapting output/Arguments_renaming.out after fixing printing ofGravatar Hugo Herbelin2014-10-02
* Adapting to naming of evars.Gravatar Hugo Herbelin2014-09-27
* Reductionops: (Co)Fixpoints are always refolded during iotaGravatar Pierre Boutillier2014-09-18
* Fixing printing of @eq which was apparently wrong bug fixed by MS on Wed 10.Gravatar Hugo Herbelin2014-09-15
* Grammar: "avoiding to" isn't proper, eitherGravatar Jason Gross2014-08-25
* Upgrading output tests.Gravatar Hugo Herbelin2014-08-12
* Fixing output test-suite.Gravatar Pierre-Marie Pédrot2014-07-21
* cbn understand ! Arguments directiveGravatar Pierre Boutillier2014-06-04
* Fixing output test-suite: since universe polymorphism, the Print commandGravatar Pierre-Marie Pédrot2014-05-08
* Fixing #3293 (eta-expansion at "match" printing time was failingGravatar Hugo Herbelin2014-04-28
* Never suppress the typing constraint of bound variables whose name wasGravatar Pierre-Marie Pédrot2014-03-01
* test-suite: opaque term -> opaque proofGravatar Pierre Boutillier2014-02-28
* test-suite: New names for vars but the expected invariant is preservedGravatar Pierre Boutillier2014-02-28
* Fix output test-suite 'simpl tactic' -> 'reduction tactics'Gravatar Pierre Boutillier2014-02-28
* test-suite/output/Notations : evar number changeGravatar Pierre Boutillier2013-12-19
* Test suite: update output reference.Gravatar xclerc2013-12-02
* Print logical name rather than path (thus allowing reproducible tests).Gravatar xclerc2013-12-02
* test-suite fixupGravatar pboutill2013-11-03
* Fixing 2 output test-suites.Gravatar ppedrot2013-10-08
* Fixing some tests from the test-suite.Gravatar ppedrot2013-09-03
* Fix testsuite so that it works with STMGravatar gareuselesinge2013-08-08
* better error message for unexpected renaming (closes #2987)Gravatar gareuselesinge2013-07-29
* Updating some output tests in test-suite:Gravatar herbelin2013-05-09
* Renaming SearchAbout into Search and Search into SearchHead.Gravatar herbelin2013-04-17
* Using Parameter instead of Variable in test-suite/outputGravatar herbelin2013-04-17
* Continuation of r16346 on filtering local definitions. RefinedGravatar herbelin2013-03-30
* Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...Gravatar pboutill2013-02-25
* Added propagation of evars unification failure reasons for betterGravatar herbelin2013-02-17
* Revised the Ltac trace mechanism so that trace breaking due toGravatar herbelin2013-02-17
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
* Fixing parsing of specific primitive tokens used as notations for patternsGravatar herbelin2012-12-18
* Revised the strategy for automatic insertion of spaces when printingGravatar herbelin2012-12-04
* Update output/Search.out after hint-related extra defs in PeanoGravatar letouzey2012-11-17
* Fixing bug #2835 (the rationale for printing notations was notGravatar herbelin2012-07-21
* Minor fixes in the test-suite after my recent commitsGravatar letouzey2012-07-06
* Constrextern is allow to use partially applied notationsGravatar pboutill2012-06-14
* Fixing test-suite after last storm in Pp.Gravatar pboutill2012-06-12
* Notations are back in the "in" clause of pattern matching.Gravatar pboutill2012-05-15
* Fixing a few bugs (see #2571) related to interpretation of multiple bindersGravatar herbelin2012-04-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 05:57:38 +0000