aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
Commit message (Expand)AuthorAge
* 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
* Fixing alpha-conversion bug #2723 introduced in r12485-12486.Gravatar herbelin2012-03-20
* Noise for nothingGravatar pboutill2012-03-02
* Arguments supports extra notation scopesGravatar gareuselesinge2012-02-14
* Fix consequence of pp bugfix in testsuiteGravatar pboutill2012-01-31
* Notations with binders: Accepting using notations for functional termsGravatar herbelin2012-01-20
* Parameters in pattern first step.Gravatar pboutill2012-01-16
* Arguments: check rename even if no implicit is specifiedGravatar gareuselesinge2011-12-19
* Command Arguments: standardizing format of error messages and American spelling.Gravatar herbelin2011-12-17
* Bypassing the use of (currently unimplemented) "Show Script" in testsGravatar herbelin2011-12-17
* Adapting test Existentials to new numbering strategy of evars (r14764).Gravatar herbelin2011-12-07
* Minor fixes to ArgumentsGravatar gareuselesinge2011-12-06
* A small test for type inference (used to be a regression at some time).Gravatar herbelin2011-12-04
* Fixing superflous newline in output of About when no parameter is renamed.Gravatar herbelin2011-12-04
* Renamig support added to "Arguments"Gravatar gareuselesinge2011-11-21
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* New Arguments vernacularGravatar gareuselesinge2011-11-21
* First attempt at making Print Assumption compatible with opaque modules (fix ...Gravatar letouzey2011-10-25
* test-suite : an additional message displayed by Notation2.vGravatar letouzey2011-09-22
* Fix test-suite for s/Defining '\1' as keyword/Identifier '\1' now a keyword/.Gravatar letouzey2011-09-22
* Fixing printing bug with last trailing non-maximally implicitGravatar herbelin2011-08-10
* Partly revert commit r14389 about relaxing the condition for being a keywordGravatar herbelin2011-08-10
* Be a bit less aggressive in declaring idents as keywords in notationsGravatar herbelin2011-08-08
* or_introl is now too complicated for basic tests of test-suite/output/PrintIn...Gravatar pboutill2011-07-26
* This adds two option tables 'Printing Record' and 'Printing Constructor'Gravatar herbelin2011-07-16
* Make Notation works with anonymous-level "Type".Gravatar herbelin2011-06-08
* test-suite: no more ..._beq in the output of the search testsGravatar letouzey2011-05-16
* Fix order in Search tests.Gravatar letouzey2011-05-16
* Fixes in the test-suite after modularisation of ZArith and coGravatar letouzey2011-05-06
* Typo in test InitSyntax.outGravatar herbelin2011-04-29
* Fixed notation printing bug when curly brackets are involved (requestsGravatar herbelin2011-04-28
* Fixing output of Notations2.v test messed up in r14060Gravatar herbelin2011-04-27
* Fixing and completing interpretation of let's in notations for iterated binders.Gravatar herbelin2011-04-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 13:03:41 +0000