coq - The formal proof system

Age	Commit message (Expand)	Author
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
2010-01-29	minor change in test-suite/output/NumberSyntax.out: a BigN.t_ instead of BigN.t	letouzey
2009-12-24	In "simpl c" and "change c with d", c can be a pattern.	herbelin
2009-12-03	Still continuing r12485-12486, r12549, r12556 (cleaning around name generation)	herbelin
2009-12-02	Continuing r12485-12486 and r12549 (cleaning around name generation)	herbelin
2009-12-01	Continuing r12485-12486 (cleaning around name generation)	herbelin
2009-11-12	BigQ / BigN / BigZ syntax and scope improvements (sequel to 12504)	letouzey
2009-11-12	Repair interpretation of numeral for BigQ, add a printer (close #2160)	letouzey
2009-11-11	Improving abbreviations/notations + backtrack of semantic change in r12439	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-04-25	- Fixing #2090 (occur check missing when trying to solve evar-evar equation).	herbelin
2009-04-20	Fix test output mentionning an existential number that changed.	msozeau
2009-03-30	Add tests for quote	glondu
2009-02-06	Fixing #2044 (bad printing of primitive notation at the head of	herbelin
2009-01-19	The initial state evar numbering increased. Fix output message in a test.	puech
2009-01-13	- Standardized prefix use of "Local"/"Global" modifiers as decided in	herbelin