coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Adding a new syntax for BeginSubproof and EndSubproof, namely { and }.	courtieu	2011-07-05
*	Break circular dependency Proof_global -> Vernacexpr -> Proof_global.	aspiwack	2011-05-17
*	New option [Set Bullet Behavior] allows to select the behaviour of bullets.	aspiwack	2011-05-13
*	G_vernac can be parsed without grammar.cma	letouzey	2011-04-26
*	Revert "Add [Polymorphic] flag for defs"	msozeau	2011-04-13
*	Add [Polymorphic] flag for defs	msozeau	2011-04-13
*	Add 'Existing Instances' declaration to declare multiple instances at once.	letouzey	2011-04-06
*	- Remove useless grammar rule	msozeau	2011-03-23
*	- Add modulo_delta_types flag for unification to allow full	msozeau	2011-03-13
*	- Fix treatment of globality flag for typeclass instance hints (they	msozeau	2011-02-14
*	Annotations at functor applications:	letouzey	2011-02-11
*	A fine-grain control of inlining at functor application via priority levels	letouzey	2011-01-31
*	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey	2011-01-28
*	Add "Print Sorted Universes"	glondu	2011-01-11
*	Remove obsolete script univdot, update dev doc about universes	glondu	2010-12-24
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Don't interpret VMcast as an ordinary type cast in Definition a := t <: T.	herbelin	2010-12-09
*	SearchAbout: who has never been annoyed by the [ ] syntax ?	letouzey	2010-11-19
*	Export the "bullet" grammar entry	glondu	2010-10-08
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	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-22
*	Fixed parsing of "Generalizable Variable A" ("Variable" turns to be a keyword).	herbelin	2010-07-18
*	Using vernac parsing for Function	jforest	2010-06-08
*	A new command Compute foo, shortcut for Eval vm_compute in foo	letouzey	2010-06-04
*	Added command "Locate Ltac qid".	herbelin	2010-06-03
*	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-05-19
*	Fail: a way to check that a command is refused without blocking a script	letouzey	2010-04-30
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	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-04-22
*	Several bug-fixes and improvements of coqdoc	herbelin	2010-03-29
*	Fixes in rewrite and a Elimination/Case to Scheme:	msozeau	2010-03-06
*	New command Declare Reduction <id> := <conv_expr>.	letouzey	2010-01-28
*	Variant !F M for functor application that does not honor the Inline declarations	letouzey	2010-01-17
*	Include can accept both Module and Module Type	letouzey	2010-01-07
*	Specific syntax for Instances in Module Type: Declare Instance	letouzey	2010-01-04
*	Fix "Existing Instance" to handle globality information and "Existing	msozeau	2009-12-27
*	Migration of ProtectedToplevel and Line_oriented_parser into new contrib Inte...	letouzey	2009-12-08
*	No more specific syntax "Include Self" for inclusion of partially-applied fun...	letouzey	2009-12-07
*	Added support for definition of fixpoints using tactics.	herbelin	2009-11-27
*	Module subtyping : allow many <: and module type declaration with <:	letouzey	2009-11-18
*	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-16
*	Document Generalizable Variables, and change syntax to	msozeau	2009-11-15
*	Added support for multiple where-clauses in Inductive and co (see wish #2163).	herbelin	2009-11-11
*	Misc fixes.	msozeau	2009-11-06