coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Adding the type infrastructure to handle properly API management of options	ppedrot	2011-11-18
*	Fix parsing of :>> and backtrack correctly on the cache of hints for local co...	msozeau	2011-11-18
*	Added a printing function to handle single evars	ppedrot	2011-11-18
*	Restore backward compatibility. ":>" declares subinstances in Class declarati...	msozeau	2011-11-18
*	Fixing bug #2640 and variants of it (inconsistency between when and	herbelin	2011-11-17
*	Merge subinstances branch by me and Tom Prince.	msozeau	2011-11-17
*	Fixing beautification of "thm_token" (missing space) + improvements.	herbelin	2011-11-16
*	Allow "\|_=>_" in "match" in patterns, no more forced enumeration of constructors	letouzey	2011-11-07
*	Remove dynamic stuff from constr_expr and glob_constr	glondu	2011-10-28
*	Applying Tom Prince's patch to support parametric "constructor n" in	herbelin	2011-10-25
*	First attempt at making Print Assumption compatible with opaque modules (fix ...	letouzey	2011-10-25
*	Various simplifications about constant_of_delta and mind_of_delta	letouzey	2011-10-11
*	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