coq - The formal proof system

Age	Commit message (Expand)	Author
2009-10-14	Improved tactic "order" in OrderedType	letouzey
2009-10-13	Made implicit arguments of Operators_Properties.v local	herbelin
2009-10-13	Typos.	gmelquio
2009-10-13	Better handling of emphasis.	msozeau
2009-10-13	MSets: a new generation of FSets	letouzey
2009-10-09	Fix bug #2162 and a name clashing bug in generalized binders.	msozeau
2009-10-09	Fix a typo(?) in previous commit	letouzey
2009-10-08	Fixed clash names in Relations (see bug report #2152) and make names	herbelin
2009-10-08	Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'	letouzey
2009-10-08	Implicit argument of Logic.eq become maximally inserted	letouzey
2009-10-08	Fixed a bug introduced in revision 12265.	herbelin
2009-10-07	Fix for missing hypotesae in XML proof tree export.	cek
2009-10-06	Fixed installation of Coqide interface/library files (bug #2147).	gmelquio
2009-10-06	Relaxed error severity when encountering unknown library objects or tactic	gmelquio
2009-10-05	Correctly do backtracking during type class resolution even if only new	msozeau
2009-10-05	Revert "kills the old backtracking framework and replaces it with"	vgross
2009-10-04	Changed the way to support compatibility with previous versions.	herbelin
2009-10-04	Removal of trailing spaces.	serpyc
2009-10-04	Some new lemmas on max and min and a fix for a wrongly stated lemma in r12358.	herbelin
2009-10-03	Fixed small name freshness bug in Functional Scheme ("Heq" name was	herbelin
2009-10-03	A few additions in Min.v.	herbelin
2009-10-03	Added option "Unset Dependent Propositions Elimination" to protect	herbelin
2009-09-29	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-28	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-27	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-26	Fixed a hole in glob_tactic that allowed some Ltac code to refer to	herbelin
2009-09-24	Micromega doc : psatz Z -> psatz Z 2	fbesson
2009-09-23	Ltac doc: only variables are accepted as message_token	glondu
2009-09-22	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-21	Update link to "Recursive Make Considered Harmful"	glondu
2009-09-20	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-18	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-17	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