coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	A new mechanism to handle errors.	aspiwack	2011-05-13
*	New option [Set Bullet Behavior] allows to select the behaviour of bullets.	aspiwack	2011-05-13
*	Print Module (Type) M now tries to print more details	letouzey	2011-05-11
*	Pcoq.ml4: fix a typo in a comment to please ocamldoc	letouzey	2011-04-26
*	G_vernac can be parsed without grammar.cma	letouzey	2011-04-26
*	Fixing bug in printing let-in binders in fix/cofix	herbelin	2011-04-24
*	Revert "Add [Polymorphic] flag for defs"	msozeau	2011-04-13
*	Add [Polymorphic] flag for defs	msozeau	2011-04-13
*	Made warning about ending comments in string less intrusive so as to support	herbelin	2011-04-08
*	Fixing multiple printing bugs with "Notation f x := ..."	herbelin	2011-04-08
*	Add 'Existing Instances' declaration to declare multiple instances at once.	letouzey	2011-04-06
*	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey	2011-04-03
*	- Remove useless grammar rule	msozeau	2011-03-23
*	A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> seconds	letouzey	2011-03-18
*	- Add modulo_delta_types flag for unification to allow full	msozeau	2011-03-13
*	Reverted commit r13893 about propagation of more informative	herbelin	2011-03-07
*	Added propagation of evars unification failure reasons for better	herbelin	2011-03-07
*	Forgotten removal of ',' in 'fun' rule: it has to come with the lambda notation	herbelin	2011-03-05
*	- 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
*	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