index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
output
Commit message (
Expand
)
Author
Age
*
Notations are back in the "in" clause of pattern matching.
pboutill
2012-05-15
*
Fixing a few bugs (see #2571) related to interpretation of multiple binders
herbelin
2012-04-06
*
Fixing alpha-conversion bug #2723 introduced in r12485-12486.
herbelin
2012-03-20
*
Noise for nothing
pboutill
2012-03-02
*
Arguments supports extra notation scopes
gareuselesinge
2012-02-14
*
Fix consequence of pp bugfix in testsuite
pboutill
2012-01-31
*
Notations with binders: Accepting using notations for functional terms
herbelin
2012-01-20
*
Parameters in pattern first step.
pboutill
2012-01-16
*
Arguments: check rename even if no implicit is specified
gareuselesinge
2011-12-19
*
Command Arguments: standardizing format of error messages and American spelling.
herbelin
2011-12-17
*
Bypassing the use of (currently unimplemented) "Show Script" in tests
herbelin
2011-12-17
*
Adapting test Existentials to new numbering strategy of evars (r14764).
herbelin
2011-12-07
*
Minor fixes to Arguments
gareuselesinge
2011-12-06
*
A small test for type inference (used to be a regression at some time).
herbelin
2011-12-04
*
Fixing superflous newline in output of About when no parameter is renamed.
herbelin
2011-12-04
*
Renamig support added to "Arguments"
gareuselesinge
2011-11-21
*
theories/, plugins/ and test-suite/ ported to the Arguments vernacular
gareuselesinge
2011-11-21
*
New Arguments vernacular
gareuselesinge
2011-11-21
*
First attempt at making Print Assumption compatible with opaque modules (fix ...
letouzey
2011-10-25
*
test-suite : an additional message displayed by Notation2.v
letouzey
2011-09-22
*
Fix test-suite for s/Defining '\1' as keyword/Identifier '\1' now a keyword/.
letouzey
2011-09-22
*
Fixing printing bug with last trailing non-maximally implicit
herbelin
2011-08-10
*
Partly revert commit r14389 about relaxing the condition for being a keyword
herbelin
2011-08-10
*
Be a bit less aggressive in declaring idents as keywords in notations
herbelin
2011-08-08
*
or_introl is now too complicated for basic tests of test-suite/output/PrintIn...
pboutill
2011-07-26
*
This adds two option tables 'Printing Record' and 'Printing Constructor'
herbelin
2011-07-16
*
Make Notation works with anonymous-level "Type".
herbelin
2011-06-08
*
test-suite: no more ..._beq in the output of the search tests
letouzey
2011-05-16
*
Fix order in Search tests.
letouzey
2011-05-16
*
Fixes in the test-suite after modularisation of ZArith and co
letouzey
2011-05-06
*
Typo in test InitSyntax.out
herbelin
2011-04-29
*
Fixed notation printing bug when curly brackets are involved (requests
herbelin
2011-04-28
*
Fixing output of Notations2.v test messed up in r14060
herbelin
2011-04-27
*
Fixing and completing interpretation of let's in notations for iterated binders.
herbelin
2011-04-25
*
Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".
herbelin
2011-04-15
*
Fixing multiple printing bugs with "Notation f x := ..."
herbelin
2011-04-08
*
Did that adding a rule for printing applications as "f(x)" works.
herbelin
2011-03-31
*
Remove some weird syntax "fun ... ," that used to be accepted (cf r13876)
letouzey
2011-03-16
*
Adapt test-suite/output/Extraction_matchs_2413 to new indentation of extraction
letouzey
2011-03-16
*
Some fixes of the test-suite scripts
letouzey
2011-02-21
*
Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)
letouzey
2010-12-21
*
test-suite: fix output/Existentials.out
glondu
2010-10-06
*
Test for non-regression of the display bug fixed in r13486.
herbelin
2010-10-03
*
Added multiple implicit arguments rules per name.
herbelin
2010-10-03
*
Making display of various informations about constants more modular:
herbelin
2010-10-03
*
Extension of the recursive notations mechanism
herbelin
2010-07-22
*
Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).
herbelin
2010-06-18
*
Added printing of recursive notations in cases pattern (supported by wish 2248).
herbelin
2010-06-14
*
Backported r13068 to branch v8.3 (whd_betaiota on inferred return
herbelin
2010-06-04
*
Fixed some printing bugs.
herbelin
2010-04-18
[next]