coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Applied patches proposed suggested by Hendrik Tews to fix existential	courtieu	2011-12-18
*	Removing PrintConstr debugging entry in g_proof.ml4 which was not	herbelin	2011-12-18
*	A pass on warning printings. Made systematic the use of msg_warning so	herbelin	2011-12-17
*	Improving pretty-printing of Ltac functions.	herbelin	2011-12-17
*	Fixing previous commit which was bugging on tactics preceded by goal number (...	courtieu	2011-12-16
*	Moving bullets (-, +, *) into stand-alone commands instead of being	courtieu	2011-12-16
*	Proof using ...	gareuselesinge	2011-12-12
*	Makefile: force the installation of all .cmi (and remove some obsolete .mli)	letouzey	2011-12-08
*	Fixing grammar resetting bug in the presence of levels initially empty	herbelin	2011-12-07
*	Minor fixes to Arguments	gareuselesinge	2011-12-06
*	Fixing superflous newline in output of About when no parameter is renamed.	herbelin	2011-12-04
*	Continuing r14747 being actually incomplete (flushing warnings and	herbelin	2011-11-30
*	Preventing Implicit Arguments warning to be shown in non verbose mode	herbelin	2011-11-30
*	Added a DEPRECATED flag in declaration of options. For now only two options a...	ppedrot	2011-11-24
*	In emacs mode, prints a list of the dependent existential variables introduced	aspiwack	2011-11-23
*	Renamig support added to "Arguments"	gareuselesinge	2011-11-21
*	New Arguments vernacular	gareuselesinge	2011-11-21
*	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