coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Term: Refactoring of hashconsing	puech	2011-07-29
*	Oversight in revision 14292.	pboutill	2011-07-27
*	Partial revert of r14292	pboutill	2011-07-26
*	Add a syntax entry for fully applied constructor pattern	pboutill	2011-07-22
*	Adding a new syntax for BeginSubproof and EndSubproof, namely { and }.	courtieu	2011-07-05
*	Revert "Check if recursive calls are guarded before printing "Proof completed"."	pboutill	2011-06-10
*	Check if recursive calls are guarded before printing "Proof completed".	herbelin	2011-05-26
*	Made the emacs-U option deprecated. Also removed the old code	courtieu	2011-05-24
*	Restore display of notation when printing an inductive such as sig	letouzey	2011-05-21
*	Break circular dependency Proof_global -> Vernacexpr -> Proof_global.	aspiwack	2011-05-17
*	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