coq - The formal proof system

Age	Commit message (Expand)	Author
2010-03-06	Fixes in rewrite and a Elimination/Case to Scheme:	msozeau
2010-03-04	Makefile: the .ml of .ml4 are now produced explicitely (in binary ast form)	letouzey
2010-01-28	New command Declare Reduction <id> := <conv_expr>.	letouzey
2010-01-17	Variant !F M for functor application that does not honor the Inline declarations	letouzey
2010-01-12	g_decl_mode: 'by' is now a keyword	letouzey
2010-01-08	* Segmenttree: New. A very simple implementation of segment trees.	regisgia
2010-01-07	Include can accept both Module and Module Type	letouzey
2010-01-06	"by" becomes officially a reserved keyword of Coq (fixes "rewrite ... at ... ...	letouzey
2010-01-04	Specific syntax for Instances in Module Type: Declare Instance	letouzey
2009-12-30	Fixing bug #2146 (broken selection of occurrences in "change").	herbelin
2009-12-29	Fixing precedence while printing patterns in Ltac (was modified in r12607)	herbelin
2009-12-27	Fix "Existing Instance" to handle globality information and "Existing	msozeau
2009-12-24	In "simpl c" and "change c with d", c can be a pattern.	herbelin
2009-12-24	Opened the possibility to type Ltac patterns but it is not fully functional yet	herbelin
2009-12-21	Generic support for open terms in tactics	herbelin
2009-12-20	* Rewrite [classify_unicode] using standard unicode tables.	regisgia
2009-12-19	Made the interpretation levels rlevel/glevel/tlevel truly phantom	herbelin
2009-12-13	Deactivating printing of {\| \|} for records when option Printing All is set.	herbelin
2009-12-13	Fixing bug in printing option as of remember and generalize	herbelin
2009-12-08	Migration of ProtectedToplevel and Line_oriented_parser into new contrib Inte...	letouzey
2009-12-07	No more specific syntax "Include Self" for inclusion of partially-applied fun...	letouzey
2009-11-27	Added support for definition of fixpoints using tactics.	herbelin
2009-11-18	Module subtyping : allow many <: and module type declaration with <:	letouzey
2009-11-16	New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))	letouzey
2009-11-16	Include Self (Type) Foo: applying a (Type) Functor to the current context	letouzey
2009-11-15	Document Generalizable Variables, and change syntax to	msozeau
2009-11-11	Added support for multiple where-clauses in Inductive and co (see wish #2163).	herbelin
2009-11-11	Improving abbreviations/notations + backtrack of semantic change in r12439	herbelin
2009-11-09	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin
2009-11-06	Misc fixes.	msozeau
2009-11-04	Fixed record syntax "{\|x=...; y=...\|}" so that it works with qualified names.	gmelquio
2009-10-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-10-28	Module type expressions of the form (Fsig X) with Definition foo := bar are n...	soubiran
2009-10-27	Add a new vernacular command for controling implicit generalization of	msozeau
2009-10-26	New cleaning phase of the Local/Global option management	herbelin
2009-10-25	Restore (and test) broken chaining of lemmas in "apply in" in presence	herbelin
2009-10-25	fixed bug in Czar grammar	corbinea
2009-10-25	Improved the treatment of Local/Global options (noneffective Local on	herbelin
2009-10-21	This big commit addresses two problems:	soubiran
2009-10-17	Fixed a notation bug when extending binder_constr with empty levels	herbelin
2009-10-04	Removal of trailing spaces.	serpyc
2009-09-29	Add support for Local Declare ML Module	glondu
2009-09-27	Complement to 12347 and 12348 on the extended syntax of case/elim.	herbelin
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-17	Delete trailing whitespaces in all .{v,ml} files	glondu
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	Generalized the possibility to refer to a global name by a notation	herbelin
2009-09-10	Added syntax "exists bindings, ..., bindings" for iterated "exists".	herbelin