coq - The formal proof system

Age	Commit message (Expand)	Author
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
2009-09-17	Clarify documentation of ltac repeat	glondu
2009-09-15	- 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-14	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-13	- Inductive types in the "using" option of auto/eauto/firstorder are	herbelin
2009-09-11	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-10	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-09	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-08	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-07	ajout CVC3; ajout traduction des reels	marche
2009-09-04	Incorporate coqdoc changes by the UPenn team (B.Pierce, C. Casinghino,	msozeau
2009-09-03	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