coq - The formal proof system

Age	Commit message (Expand)	Author
2012-03-02	Noise for nothing	pboutill
2012-02-14	Arguments supports extra notation scopes	gareuselesinge
2012-01-31	Fix consequence of pp bugfix in testsuite	pboutill
2012-01-20	Notations with binders: Accepting using notations for functional terms	herbelin
2012-01-16	Parameters in pattern first step.	pboutill
2011-12-19	Arguments: check rename even if no implicit is specified	gareuselesinge
2011-12-17	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-07	Adapting test Existentials to new numbering strategy of evars (r14764).	herbelin
2011-12-06	Minor fixes to Arguments	gareuselesinge
2011-12-04	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-11-21	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-10-25	First attempt at making Print Assumption compatible with opaque modules (fix ...	letouzey
2011-09-22	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-08-10	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-08	Be a bit less aggressive in declaring idents as keywords in notations	herbelin
2011-07-26	or_introl is now too complicated for basic tests of test-suite/output/PrintIn...	pboutill
2011-07-16	This adds two option tables 'Printing Record' and 'Printing Constructor'	herbelin
2011-06-08	Make Notation works with anonymous-level "Type".	herbelin
2011-05-16	test-suite: no more ..._beq in the output of the search tests	letouzey
2011-05-16	Fix order in Search tests.	letouzey
2011-05-06	Fixes in the test-suite after modularisation of ZArith and co	letouzey
2011-04-29	Typo in test InitSyntax.out	herbelin
2011-04-28	Fixed notation printing bug when curly brackets are involved (requests	herbelin
2011-04-27	Fixing output of Notations2.v test messed up in r14060	herbelin
2011-04-25	Fixing and completing interpretation of let's in notations for iterated binders.	herbelin
2011-04-15	Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".	herbelin
2011-04-08	Fixing multiple printing bugs with "Notation f x := ..."	herbelin
2011-03-31	Did that adding a rule for printing applications as "f(x)" works.	herbelin
2011-03-16	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-02-21	Some fixes of the test-suite scripts	letouzey
2010-12-21	Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)	letouzey
2010-10-06	test-suite: fix output/Existentials.out	glondu
2010-10-03	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-07-22	Extension of the recursive notations mechanism	herbelin
2010-06-18	Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).	herbelin
2010-06-14	Added printing of recursive notations in cases pattern (supported by wish 2248).	herbelin
2010-06-04	Backported r13068 to branch v8.3 (whd_betaiota on inferred return	herbelin
2010-04-18	Fixed some printing bugs.	herbelin
2010-04-10	Optimized need for delimiters when disjoint scopes for strings and	herbelin
2010-03-11	Minimal test suite for search commands	puech
2010-02-13	Fix NumbersSyntax.out	letouzey