coq - The formal proof system

Age	Commit message (Expand)	Author
2009-04-08	- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixing	herbelin
2009-03-29	Avoid inadvertent declaration of "on" as a keyword. New syntax is	msozeau
2009-03-28	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau
2009-03-27	Parsing files for numerals (+ ascii/string) moved into plugins	letouzey
2009-03-27	Remove unused mli files	letouzey
2009-03-23	- Fixed bug 2058 (as much as possible - the syntax of "pose (f binders := ...)"	herbelin
2009-03-20	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey
2009-03-16	Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"	herbelin
2009-03-09	Optionally list opaque constants in addition to axions/variables in	msozeau
2009-03-04	commande Timeout + compaction des traces de debug_tactic	barras
2009-02-03	Do not reserve the keyword "Infer".	puech
2009-01-19	Les records déclarés avec Record ne peuvent plus être récursifs (le	aspiwack
2009-01-19	- Structuring Numbers and fixing Setoid in stdlib's doc.	herbelin
2009-01-18	Getting rid of the previous implementation of setoid_rewrite which was	msozeau
2009-01-18	Last changes in type class syntax:	msozeau
2009-01-17	DISCLAIMER	puech
2009-01-14	Fixing #1960 (xml bug with external on goal variable) and #1961	herbelin
2009-01-14	Fixing/improving management of uniform prefix Local and Global	herbelin
2009-01-13	- Standardized prefix use of "Local"/"Global" modifiers as decided in	herbelin
2009-01-07	Fixing a cosmetic tactic printer bug in passing	herbelin
2009-01-02	- Temptative change to notations like "as [\|n H]_eqn" or "as [\|n H]_eqn:H",	herbelin
2008-12-31	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin
2008-12-29	- Added support for subterm matching in SearchAbout.	herbelin
2008-12-28	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin
2008-12-24	- coq_makefile: target install now respects the original tree structure	herbelin
2008-12-14	Generalized binding syntax overhaul: only two new binders: `() and `{},	msozeau
2008-12-09	About "apply in":	herbelin
2008-11-26	closed bug 1898: fold x in x; added a reordering primitive tactic	barras
2008-11-23	Fixed bug #2006 (type constraint on Record was not taken into account) +	herbelin
2008-11-22	Fixed bug in VernacExtend printing + missing vernacular printing rules +	herbelin
2008-11-10	Fix mixup between Record, Structure and Class by adding a new variant for	msozeau
2008-11-09	Oops... forgot to commit a file related to r11561.	msozeau
2008-11-09	More factorization of inductive/record and typeclasses: move class	msozeau
2008-11-09	- Fixed bug 1968 (inversion failing due to a Not_found bug introduced in	herbelin
2008-11-05	Move Record desugaring to constrintern and add ability to use notations	msozeau
2008-11-05	Nouvelle syntaxe pour écrire des records (co)inductifs :	aspiwack
2008-10-31	allowed patternidents starting with an '_'	amahboub
2008-10-30	The lexer is changer to break former PATTERNIDENT into two tokens.	amahboub
2008-10-26	Fixes and refinements regarding occurrence selection:	herbelin
2008-10-23	Open notation for declaring record instances.	msozeau
2008-10-23	Generalized implementation of generalization.	msozeau
2008-10-22	A much better implementation of implicit generalization:	msozeau
2008-10-22	Affichage des notations récursives:	herbelin
2008-10-21	duplicated open of Ppconstr	letouzey
2008-10-20	Renommage "Global Instance" en "Instance Global" pour uniformisation	herbelin
2008-10-19	- Export de pattern_ident vers les ARGUMENT EXTEND and co.	herbelin
2008-10-15	Report des commits 11417 et 11437 de la v8.2	soubiran
2008-10-11	Backporting 11445 from 8.2 to trunk (negative conditions in	herbelin
2008-09-14	Add user syntax for creating hint databases [Create HintDb foo	msozeau
2008-09-07	Add the ability to declare [Hint Extern]'s with no pattern.	msozeau