coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	This big commit addresses two problems:	soubiran	2009-10-21
*	Fix bug #2162 and a name clashing bug in generalized binders.	msozeau	2009-10-09
*	Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'	letouzey	2009-10-08
*	Fix for missing hypotesae in XML proof tree export.	cek	2009-10-07
*	Removal of trailing spaces.	serpyc	2009-10-04
*	Fixed small name freshness bug in Functional Scheme ("Heq" name was	herbelin	2009-10-03
*	Add support for Local Declare ML Module	glondu	2009-09-29
*	Fix the stdlib doc compilation + switch all .v file to utf8	letouzey	2009-09-28
*	Only one "in" clause in "destruct" even for a multiple "destruct".	herbelin	2009-09-20
*	micromega: better handling of exponentiation + correction of test-suite termi...	fbesson	2009-09-18
*	Remove useless Liboject.export_function field	glondu	2009-09-17
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Dont't forget to update the state or an obligation tactic assignment may	msozeau	2009-09-15
*	Stop using [obligation_tactic] from Program.Tactics as the default	msozeau	2009-09-15
*	Backtrack on the forced discharge of type class variables introduced	msozeau	2009-09-14
*	- Inductive types in the "using" option of auto/eauto/firstorder are	herbelin	2009-09-13
*	Generalized the possibility to refer to a global name by a notation	herbelin	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
*	Misc fixes:	msozeau	2009-09-10
*	Added syntax "exists bindings, ..., bindings" for iterated "exists".	herbelin	2009-09-10
*	Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvements	letouzey	2009-09-09
*	ajout CVC3; ajout traduction des reels	marche	2009-09-07
*	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
*	update for why 2.19	marche	2009-08-28
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 85f007b7-540e-0...	fbesson	2009-08-25
*	new csdp cache + improved error message	fbesson	2009-08-20
*	new csdp cache + improved error message	fbesson	2009-08-20
*	+Fix interface.	aspiwack	2009-08-14
*	Death of "survive_module" and "survive_section" (the first one was	herbelin	2009-08-13
*	Infix (r12268 continued)	herbelin	2009-08-11
*	Cleaning of Nametab continued + fixed a compilation bug in previous commit.	herbelin	2009-08-06
*	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin	2009-08-06
*	Added "etransitivity".	herbelin	2009-08-03
*	Improved parameterization of Coq:	herbelin	2009-08-02
*	addition of lia.cache - csdp.cache is now handled by micromega not csdpcert	fbesson	2009-07-31
*	micromega : Better parsing of formulae - smaller proof terms for Z - redesign...	fbesson	2009-07-30
*	Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"	letouzey	2009-07-24
*	Use camlp4 to accept some specific non-exhaustive patterns in groebner	letouzey	2009-07-20
*	Move some examples for groebner into a test-suite file	letouzey	2009-07-20
*	Use the proper unification flags in e_exact. This makes exact fail a bit	msozeau	2009-07-09
*	repport of commit r12221	jforest	2009-07-04
*	Miscellaneous practical commits:	herbelin	2009-06-29
*	Fix bug introduced by last revision, subtac_cases was returning the	msozeau	2009-06-29
*	Abstract the tycon by the matched terms when turning them into variables	msozeau	2009-06-28
*	Improve return predicate inference by making the return type dependent	msozeau	2009-06-28
*	Fixes for r12197, the refined evars were not returned in case fail_evar	msozeau	2009-06-22
*	Use more consistent resolution parameters in Program and regular typing	msozeau	2009-06-18
*	Fallback on not using [fix_proto] if the right imports aren't there, the	msozeau	2009-06-17