coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	In Coq_config: get rid of coqsrc and make coqlib optional	glondu	2011-09-27
*	Added support for referring to subterms of the goal by pattern.	herbelin	2011-09-26
*	Moving implicit tactic support from Tacinterp to Pfedit and final evar	herbelin	2011-09-26
*	Re-allowing assumptions during proofs seems safe now (fix #2411)	letouzey	2011-09-15
*	Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...	aspiwack	2011-09-12
*	Coqide: new backtracking code, based on the Backtrack command	letouzey	2011-09-05
*	Ide_intf: slight reorganisation of the IDE api	letouzey	2011-09-05
*	Lib.node: merge OpenedModtype and OpenedModule, same for Closed...	letouzey	2011-09-05
*	Remove code concerning the obsolete Set/Unset Undo	letouzey	2011-09-05
*	Quick improvement of some error messages related to module application	herbelin	2011-08-30
*	Clarifying that only identifiers are advertised to be turned into keywords	herbelin	2011-08-23
*	Misc improvements concerning "Show Match" and its coqide equivalent	letouzey	2011-08-18
*	SearchAbout and similar: add a customizable blacklist	letouzey	2011-08-11
*	Improving error message about coinductive guard (old "cases" is now "match")	herbelin	2011-08-10
*	Partly revert commit r14389 about relaxing the condition for being a keyword	herbelin	2011-08-10
*	Moved the declaration of "Classic" being the default proof mode to coqtop.ml ...	aspiwack	2011-08-09
*	Be a bit less aggressive in declaring idents as keywords in notations	herbelin	2011-08-08
*	Fix nf_evars_undefined use in pr_constraints	msozeau	2011-08-03
*	Class: generic equality on constr replaced by destructors	puech	2011-07-29
*	Ide_slave: same attributes for { } and Focus/Unfocus (fix coqide display)	letouzey	2011-07-28
*	This option disables the use of the '{\| field := ... \|}' notation	herbelin	2011-07-16
*	Keep obligation source information in Program	msozeau	2011-06-30
*	Cleaning debugging printer relative to new proof engine. In	herbelin	2011-06-21
*	Add compatibility option "-compat 8.3".	herbelin	2011-06-20
*	Relaxed the constraint introduced in r14190 that froze the existing	herbelin	2011-06-18
*	Fixing bug #2181 (Class mechanism can create dependencies over unnamed	herbelin	2011-06-14
*	Another bug of Scheme Induction (generated names dep/nodep were swapped).	herbelin	2011-06-13
*	Fixing an anomaly in Scheme Induction.	herbelin	2011-06-13
*	Made the emacs-U option deprecated. Also removed the old code	courtieu	2011-05-24
*	Coqide: allow the use of Abort (grant wish #2357)	letouzey	2011-05-18
*	More work on error handling	letouzey	2011-05-17
*	Break circular dependency Proof_global -> Vernacexpr -> Proof_global.	aspiwack	2011-05-17
*	Repair the "Fail" command after recent changes in exception handling	letouzey	2011-05-16
*	turn the automatic generation of boolean equality	vsiles	2011-05-16
*	Turning Sys_error into error by default instead of anomaly. After all,	herbelin	2011-05-15
*	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
*	Merge branch 'subclasses' into coq-trunk	msozeau	2011-05-05
*	Fixed a bug causing inconsistent states during proof editting.	aspiwack	2011-04-29
*	coqtop -config returns coq returns coq environments at exection time	pboutill	2011-04-28
*	Fixed notation printing bug when curly brackets are involved (requests	herbelin	2011-04-28
*	Coqide: better handling of stdout/stderr in win32	letouzey	2011-04-21
*	Add a flag to control betaiota reduction during unification to maintain backw...	msozeau	2011-04-18
*	Add directories in COQPATH to search path.	herbelin	2011-04-14
*	Reorder search path order, so the standard library is search last.	herbelin	2011-04-14
*	Revert "Add [Polymorphic] flag for defs"	msozeau	2011-04-13
*	- Make typeclass transparency information directly available	msozeau	2011-04-13
*	- Remove create_evar_defs	msozeau	2011-04-13
*	Add [Polymorphic] flag for defs	msozeau	2011-04-13