coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey	2011-01-28
*	Fix compilation with camlp5 (Closes: #2487)	glondu	2011-01-25
*	Add "Print Sorted Universes"	glondu	2011-01-11
*	ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPED	glondu	2010-12-25
*	Avoid "open {Pcoq,Extrawit}" clauses in expansion of EXTEND commands	glondu	2010-12-25
*	More {raw => glob} changes for consistency	glondu	2010-12-24
*	Remove obsolete script univdot, update dev doc about universes	glondu	2010-12-24
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	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
*	adapt slighlty r13642 to support both camlp4 and camlp5-5 and camlp5-6	letouzey	2010-11-18
*	Support for camlp5 6.02.0 (Closes: #2432)	glondu	2010-11-16
*	About "unsupported" unicode characters in notations.	herbelin	2010-10-17
*	Backporting r13521 from branch 8.3 to trunk (fixing bug #2406, looping	herbelin	2010-10-11
*	Export the "bullet" grammar entry	glondu	2010-10-08
*	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