coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Optimized need for delimiters when disjoint scopes for strings and	herbelin	2010-04-10
*	Minimal test suite for search commands	puech	2010-03-11
*	Fix NumbersSyntax.out	letouzey	2010-02-13
*	minor change in test-suite/output/NumberSyntax.out: a BigN.t_ instead of BigN.t	letouzey	2010-01-29
*	In "simpl c" and "change c with d", c can be a pattern.	herbelin	2009-12-24
*	Still continuing r12485-12486, r12549, r12556 (cleaning around name generation)	herbelin	2009-12-03
*	Continuing r12485-12486 and r12549 (cleaning around name generation)	herbelin	2009-12-02
*	Continuing r12485-12486 (cleaning around name generation)	herbelin	2009-12-01
*	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-12
*	Improving abbreviations/notations + backtrack of semantic change in r12439	herbelin	2009-11-11
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	- Fixing #2090 (occur check missing when trying to solve evar-evar equation).	herbelin	2009-04-25
*	Fix test output mentionning an existential number that changed.	msozeau	2009-04-20
*	Add tests for quote	glondu	2009-03-30
*	Fixing #2044 (bad printing of primitive notation at the head of	herbelin	2009-02-06
*	The initial state evar numbering increased. Fix output message in a test.	puech	2009-01-19
*	- Standardized prefix use of "Local"/"Global" modifiers as decided in	herbelin	2009-01-13
*	Regression test for bug #1967	herbelin	2009-01-02
*	Conséquence renommage canonique de refl_equal en eq_refl.	herbelin	2009-01-02
*	Miscellaneous fixes and improvements:	herbelin	2008-12-02
*	Test case for previous commit.	msozeau	2008-11-27
*	- Correction erreur dans test output Notation.v	herbelin	2008-11-09
*	- Ajout possibilité de lancer ocamldebug sur coqide	herbelin	2008-11-07
*	11511 continued (bug in set.out + incohérence dans "Theorem with"	herbelin	2008-10-28
*	- Fixed many "Theorem with" bugs.	herbelin	2008-10-27
*	Affichage des notations récursives:	herbelin	2008-10-22
*	Correction de bugs:	herbelin	2008-08-05
*	Évolutions diverses et variées.	herbelin	2008-08-04