coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove Explain* vernacs	glondu	2010-10-06
*	Remove VernacGo	glondu	2010-10-06
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
*	Making display of various informations about constants more modular:	herbelin	2010-10-03
*	Fixed a little printing bug with "About" on an undefined constant.	herbelin	2010-10-03
*	Simplify tactic(_)-bound arguments in TACTIC EXTEND rules	glondu	2010-09-30
*	Remove some occurrences of "open Termops"	glondu	2010-09-28
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Improved printing of Unfoldable constants in hints databases (used	herbelin	2010-09-02
*	r13359 continued: removed native treatment for λ (lambda) and Π (Pi)	herbelin	2010-07-30
*	Rather quick hack to make basic unicode notations available by	herbelin	2010-07-29
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Extension of the recursive notations mechanism	herbelin	2010-07-22
*	Constrintern: unified push_name_env and push_loc_name_env; made	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
*	Finish adding out-of-the-box support for camlp4	letouzey	2010-07-09
*	Applying François' patches about Canonical Projections (see #2302 and #2334).	herbelin	2010-06-26
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	Fixing spelling: pr_coma -> pr_comma	herbelin	2010-06-12
*	Using vernac parsing for Function	jforest	2010-06-08
*	Added support for Ltac-matching terms with variables bound in the pattern	herbelin	2010-06-06
*	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
*	deporting Coq specific code from ide to toplevel.	vgross	2010-05-31
*	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
*	Discontinue support for ocaml 3.09.*	letouzey	2010-05-19
*	Missing warning flush in a lexer message + update of CHANGES	herbelin	2010-05-12
*	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
*	Removed obsolete v7->v8 translation code (function check_same_type is	herbelin	2010-04-29
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
*	Misc small fixes : warning, dep cycles, ocamlbuild...	letouzey	2010-04-26
*	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
*	Improving error messages in the presence of utf-8 characters	herbelin	2010-03-30
*	Several bug-fixes and improvements of coqdoc	herbelin	2010-03-29
*	Added automatic expansion on the left of recursive notations	herbelin	2010-03-23
*	Fixes in rewrite and a Elimination/Case to Scheme:	msozeau	2010-03-06
*	Makefile: the .ml of .ml4 are now produced explicitely (in binary ast form)	letouzey	2010-03-04
*	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
*	g_decl_mode: 'by' is now a keyword	letouzey	2010-01-12
*	* Segmenttree: New. A very simple implementation of segment trees.	regisgia	2010-01-08
*	Include can accept both Module and Module Type	letouzey	2010-01-07
*	"by" becomes officially a reserved keyword of Coq (fixes "rewrite ... at ... ...	letouzey	2010-01-06
*	Specific syntax for Instances in Module Type: Declare Instance	letouzey	2010-01-04
*	Fixing bug #2146 (broken selection of occurrences in "change").	herbelin	2009-12-30