coq - The formal proof system

Age	Commit message (Expand)	Author
2011-12-18	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-17	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-16	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-12	Proof using ...	gareuselesinge
2011-12-08	Makefile: force the installation of all .cmi (and remove some obsolete .mli)	letouzey
2011-12-07	Fixing grammar resetting bug in the presence of levels initially empty	herbelin
2011-12-06	Minor fixes to Arguments	gareuselesinge
2011-12-04	Fixing superflous newline in output of About when no parameter is renamed.	herbelin
2011-11-30	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-24	Added a DEPRECATED flag in declaration of options. For now only two options a...	ppedrot
2011-11-23	In emacs mode, prints a list of the dependent existential variables introduced	aspiwack
2011-11-21	Renamig support added to "Arguments"	gareuselesinge
2011-11-21	New Arguments vernacular	gareuselesinge
2011-11-18	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-17	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-16	Fixing beautification of "thm_token" (missing space) + improvements.	herbelin
2011-11-07	Allow "\|_=>_" in "match" in patterns, no more forced enumeration of constructors	letouzey
2011-10-28	Remove dynamic stuff from constr_expr and glob_constr	glondu
2011-10-25	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-11	Various simplifications about constant_of_delta and mind_of_delta	letouzey
2011-09-15	Names.make_mbid and co : convert from/to identifier (avoid some String.copy)	letouzey
2011-09-12	Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...	aspiwack
2011-09-05	Lib.node: merge OpenedModtype and OpenedModule, same for Closed...	letouzey
2011-08-30	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-13	New fix for is_ident_not_keyword.	herbelin
2011-08-10	Propagated information from the reduction tactics to the kernel so	herbelin
2011-08-09	In coqtop, a terminating "." must now be followed by a blank or eof.	letouzey
2011-08-08	Be a bit less aggressive in declaring idents as keywords in notations	herbelin
2011-07-29	Term: Refactoring of hashconsing	puech
2011-07-27	Oversight in revision 14292.	pboutill
2011-07-26	Partial revert of r14292	pboutill
2011-07-22	Add a syntax entry for fully applied constructor pattern	pboutill
2011-07-05	Adding a new syntax for BeginSubproof and EndSubproof, namely { and }.	courtieu
2011-06-10	Revert "Check if recursive calls are guarded before printing "Proof completed"."	pboutill
2011-05-26	Check if recursive calls are guarded before printing "Proof completed".	herbelin
2011-05-24	Made the emacs-U option deprecated. Also removed the old code	courtieu
2011-05-21	Restore display of notation when printing an inductive such as sig	letouzey
2011-05-17	Break circular dependency Proof_global -> Vernacexpr -> Proof_global.	aspiwack
2011-05-13	A new mechanism to handle errors.	aspiwack
2011-05-13	New option [Set Bullet Behavior] allows to select the behaviour of bullets.	aspiwack