coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Names.make_mbid and co : convert from/to identifier (avoid some String.copy)	letouzey	2011-09-15
*	Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...	aspiwack	2011-09-12
*	Lib.node: merge OpenedModtype and OpenedModule, same for Closed...	letouzey	2011-09-05
*	Porting Hendrik's 8.3 patch for proof tree visualization under proof	herbelin	2011-08-30
*	Quick improvement of some error messages related to module application	herbelin	2011-08-30
*	New fix for is_ident_not_keyword.	herbelin	2011-08-13
*	Propagated information from the reduction tactics to the kernel so	herbelin	2011-08-10
*	In coqtop, a terminating "." must now be followed by a blank or eof.	letouzey	2011-08-09
*	Be a bit less aggressive in declaring idents as keywords in notations	herbelin	2011-08-08
*	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