coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- Inductive types in the "using" option of auto/eauto/firstorder are	herbelin	2009-09-13
*	Addendum to revision 12323; update Makefile.common after removal of	herbelin	2009-09-11
*	Generalized the possibility to refer to a global name by a notation	herbelin	2009-09-11
*	Add doc of [Context] vernacular.	msozeau	2009-09-11
*	Added the following lemmas to homogenize Reals a bit:	gmelquio	2009-09-11
*	Removed Gappa from the external provers supported by the dp plugin. Tactic ga...	gmelquio	2009-09-11
*	- Resolve type class constraints before trying to find unresolved	msozeau	2009-09-11
*	Fixes for toc depth handling and handling of substitles from Chris Casinghino.	msozeau	2009-09-10
*	Misc fixes:	msozeau	2009-09-10
*	Added syntax "exists bindings, ..., bindings" for iterated "exists".	herbelin	2009-09-10
*	Allow setoid rewrite to rewrite in pattern-matching scrutinees or	msozeau	2009-09-09
*	Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvements	letouzey	2009-09-09
*	Stop trying to search if the relation is declared as a [RewriteRelation]	msozeau	2009-09-09
*	Update coqdoc documentation, CHANGES and add a fix for the proofbox (patch	msozeau	2009-09-08
*	Fix the bug-ridden code used to choose leibniz or generalized	msozeau	2009-09-08
*	ajout CVC3; ajout traduction des reels	marche	2009-09-07
*	Incorporate coqdoc changes by the UPenn team (B.Pierce, C. Casinghino,	msozeau	2009-09-04
*	Add --plain-comments patch by F. Garillot, which also adds	msozeau	2009-09-03
*	Support globality flag properly for "Add Morphism foo : foo_mor" syntax.	msozeau	2009-09-03
*	Remove unnecessary redefinitions of [Fix_sub] and [Fix_F_sub], as	msozeau	2009-09-03
*	Postpone checking of Local/Global to allow grammar extensions to use it	msozeau	2009-09-02
*	Stop unnecessary use of lazy values for constraints, simplifying	msozeau	2009-09-02
*	Hack to correctly get ill-formed rec body exceptions even	msozeau	2009-09-02
*	Fix notation for ~x in theories/Unicode/Utf8.v	glondu	2009-08-31
*	Fix minor spelling error	glondu	2009-08-29
*	update for why 2.19	marche	2009-08-28
*	Correction bug 2140.	soubiran	2009-08-27
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 85f007b7-540e-0...	fbesson	2009-08-25
*	Delegate _all_ doc targets to stage2	lmamane	2009-08-25
*	install-doc* are PHONY	lmamane	2009-08-25
*	New tactic to rewrite decidability lemmas when one knows which side	herbelin	2009-08-24
*	A new kind of automatically generated scheme "congr" for equality types	herbelin	2009-08-23
*	Fix a small oversight in checker commit 12288.	herbelin	2009-08-23
*	Transfers to checker ("let"s in inductive arities + Coq root read-only).	herbelin	2009-08-22
*	new csdp cache + improved error message	fbesson	2009-08-20
*	new csdp cache + improved error message	fbesson	2009-08-20
*	adds a property on map	bertot	2009-08-19
*	adds lemmas on interactions between existsb, forallb, and app	bertot	2009-08-19
*	+ csdp.cache	fbesson	2009-08-15
*	Mise à jour du document de révision de la stdlib et déplacement de la	herbelin	2009-08-14
*	+Fix interface.	aspiwack	2009-08-14
*	Ajout de la gestion de Local et Global pour les options (au sens de	aspiwack	2009-08-14
*	Added profile.cmo in grammar.cma so that any functions in one of the	herbelin	2009-08-14
*	Tried to make F1 documentation tool working in CoqIDE.	herbelin	2009-08-14
*	Death of "survive_module" and "survive_section" (the first one was	herbelin	2009-08-13
*	Made unification patch 12268 even more ad hoc (if evars remain in a	herbelin	2009-08-13
*	Ensures that let-in's in arities of inductive types work well. Maybe not	herbelin	2009-08-11
*	Ajout des .annot dans le .gitignore.	aspiwack	2009-08-11
*	Fixed extra space in printing notation { x & P } + minor other things	herbelin	2009-08-11
*	Infix (r12268 continued)	herbelin	2009-08-11