coq - The formal proof system

Age	Commit message (Expand)	Author
2011-04-26	G_vernac can be parsed without grammar.cma	letouzey
2011-04-13	Revert "Add [Polymorphic] flag for defs"	msozeau
2011-04-13	Add [Polymorphic] flag for defs	msozeau
2011-04-06	Add 'Existing Instances' declaration to declare multiple instances at once.	letouzey
2011-03-23	- Remove useless grammar rule	msozeau
2011-03-13	- Add modulo_delta_types flag for unification to allow full	msozeau
2011-02-14	- Fix treatment of globality flag for typeclass instance hints (they	msozeau
2011-02-11	Annotations at functor applications:	letouzey
2011-01-31	A fine-grain control of inlining at functor application via priority levels	letouzey
2011-01-28	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey
2011-01-11	Add "Print Sorted Universes"	glondu
2010-12-24	Remove obsolete script univdot, update dev doc about universes	glondu
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-12-09	Don't interpret VMcast as an ordinary type cast in Definition a := t <: T.	herbelin
2010-11-19	SearchAbout: who has never been annoyed by the [ ] syntax ?	letouzey
2010-10-08	Export the "bullet" grammar entry	glondu
2010-10-03	Added multiple implicit arguments rules per name.	herbelin
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-07-22	Extension of the recursive notations mechanism	herbelin
2010-07-22	Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).	herbelin
2010-07-18	Fixed parsing of "Generalizable Variable A" ("Variable" turns to be a keyword).	herbelin
2010-06-08	Using vernac parsing for Function	jforest
2010-06-04	A new command Compute foo, shortcut for Eval vm_compute in foo	letouzey
2010-06-03	Added command "Locate Ltac qid".	herbelin
2010-05-19	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey
2010-05-19	Nicer representation of tokens, more independant of camlp*	letouzey
2010-05-19	static (and shared) camlp4use instead of per-file declaration	letouzey
2010-04-30	Fail: a way to check that a command is refused without blocking a script	letouzey
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-22	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack
2010-04-22	Applying François Garillot's patch (#2261 in bug tracker) for extended	herbelin
2010-03-29	Several bug-fixes and improvements of coqdoc	herbelin
2010-03-06	Fixes in rewrite and a Elimination/Case to Scheme:	msozeau
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-07	Include can accept both Module and Module Type	letouzey
2010-01-04	Specific syntax for Instances in Module Type: Declare Instance	letouzey
2009-12-27	Fix "Existing Instance" to handle globality information and "Existing	msozeau
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-06	Misc fixes.	msozeau
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