coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Add support for Local Declare ML Module	glondu	2009-09-29
*	Remove legacy export_* functions	glondu	2009-09-29
*	kills the old backtracking framework and replaces it with	vgross	2009-09-29
*	Fix the stdlib doc compilation + switch all .v file to utf8	letouzey	2009-09-28
*	Applied patches from BSD/pkgsrc maintainer, so that Coq compiles out-of-the-box.	gmelquio	2009-09-28
*	Apply "Declare Implicit Tactic" also to terms interpreted as "open	herbelin	2009-09-27
*	Fixed a bug in the interaction between dEqThen and inject_at_positions	herbelin	2009-09-27
*	Fixed two tests that was incorrectly typed in former revisions 12348 and 12356.	herbelin	2009-09-27
*	Add a few properties about Rmin/Rmax with replication in Zmin/Zmax.	herbelin	2009-09-27
*	Fixed error message "cannot infer the type of id" in presence of	herbelin	2009-09-27
*	Delay the choice of eliminator in destruct/induction until we know if	herbelin	2009-09-27
*	Complement to 12347 and 12348 on the extended syntax of case/elim.	herbelin	2009-09-27
*	Fixed a hole in glob_tactic that allowed some Ltac code to refer to	herbelin	2009-09-26
*	Micromega doc : psatz Z -> psatz Z 2	fbesson	2009-09-24
*	Ltac doc: only variables are accepted as message_token	glondu	2009-09-23
*	Add the option to automatically introduce variables declared before the	msozeau	2009-09-22
*	Better use of transparency information for local hypotheses:	msozeau	2009-09-22
*	Update link to "Recursive Make Considered Harmful"	glondu	2009-09-21
*	Only one "in" clause in "destruct" even for a multiple "destruct".	herbelin	2009-09-20
*	Add "case as/in/using" and temporary "destruct" with n args.	herbelin	2009-09-20
*	micromega: better handling of exponentiation + correction of test-suite termi...	fbesson	2009-09-18
*	- Fixed a bug in checking that implicit arguments are all correctly	herbelin	2009-09-18
*	Replace call to where_in_path by find_file_in_path in "Locate File"	glondu	2009-09-17
*	Replace unprotected call to where_in_path by find_file_in_path	glondu	2009-09-17
*	Remove useless MonoList.v	glondu	2009-09-17
*	Remove useless Liboject.export_function field	glondu	2009-09-17
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Fix typos in comments	glondu	2009-09-17
*	Clarify documentation of ltac repeat	glondu	2009-09-17
*	- Tentatively made order-dependency wrt .vo files a full dependency	herbelin	2009-09-15
*	Fix compilation errors due to last commit.	msozeau	2009-09-15
*	Dont't forget to update the state or an obligation tactic assignment may	msozeau	2009-09-15
*	Fixed compilation error message which was no longer emacs-compliant since	herbelin	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
*	removed the double-click / proof hiding association.	vgross	2009-09-14
*	tags refactoring	vgross	2009-09-14
*	- Addition of "Reserved Infix" continued.	herbelin	2009-09-14
*	- 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