coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Added support for referring to subterms of the goal by pattern.	herbelin	2011-09-26
*	auto with nocore : disable the use of the core database (wish #2188)	letouzey	2011-09-23
*	Omega: for non-arithmetical goals, try proving False from context (wish #2236)	letouzey	2011-09-16
*	Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...	aspiwack	2011-09-12
*	Bug 2577: Second attempt to be correct.	pboutill	2011-09-01
*	Updates in CHANGES	letouzey	2011-08-18
*	Propagated information from the reduction tactics to the kernel so	herbelin	2011-08-10
*	Made CHANGES more uniformly written	herbelin	2011-08-10
*	Less ambitious application of a notation for eq_rect. We proposed	herbelin	2011-08-10
*	Typo of bug 2577	pboutill	2011-07-27
*	This adds two option tables 'Printing Record' and 'Printing Constructor'	herbelin	2011-07-16
*	This option disables the use of the '{\| field := ... \|}' notation	herbelin	2011-07-16
*	Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)	herbelin	2011-07-16
*	Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and...	herbelin	2011-07-16
*	Ensured that the transparency state is used when flag betaiota is on for apply.	herbelin	2011-06-19
*	Relaxed the constraint introduced in r14190 that froze the existing	herbelin	2011-06-18
*	Generalizing flag use_evars_pattern_unification into a flag	herbelin	2011-06-18
*	Typo in CHANGES	herbelin	2011-06-18
*	Updated CHANGES (info, Show Script, rephrasing).	herbelin	2011-06-10
*	Fixing another bug with "_" intro pattern.	herbelin	2011-06-10
*	CHANGES update	pboutill	2011-04-28
*	Coqide: try to properly send interrupts to coqtop on Win32	letouzey	2011-04-28
*	Updating CHANGES	herbelin	2011-04-27
*	Fixed a bug of destruct which was sometimes forgetting local definitions behi...	herbelin	2011-04-24
*	Add directories in COQPATH to search path.	herbelin	2011-04-14
*	Add "make full-stdlib" to make all the doc in pdf as ask by bug 2395	pboutill	2011-04-08
*	Update documentation concerning proofs loading (cf last commit)	letouzey	2011-04-03
*	CHANGES: a word about recent changes in coqide, about Ctrl-C in vm	letouzey	2011-04-01
*	Documentation of the timeout tactical (cf r13917)	letouzey	2011-03-21
*	An option "Set Default Timeout n."	letouzey	2011-03-17
*	CHANGES: mentionning quickly Separate Extraction	letouzey	2011-03-07
*	CHANGES: update of syntax for annotations of functor application	letouzey	2011-03-04
*	Extraction: improved indentation of extracted code (fix #2497)	letouzey	2011-03-04
*	Update changelogs	glondu	2011-02-11
*	Fixpoints are traverse during implicits arguments search to toplevel	pboutill	2011-02-10
*	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
*	Update CHANGES	pboutill	2011-01-07
*	First release of Vector library.	pboutill	2010-12-10
*	ZArith: for uniformity, Zdiv2 becomes Zquot2 while Zdiv2' becomes Zdiv2	letouzey	2010-12-09
*	Numbers and bitwise functions.	letouzey	2010-12-06
*	Document new tactics in CHANGES	glondu	2010-12-02
*	CHANGES: mention some changes in trunk since the 8.3 fork	letouzey	2010-11-19
*	SearchAbout: who has never been annoyed by the [ ] syntax ?	letouzey	2010-11-19
*	CHANGES: small re-sync with the one of branch v8.3	letouzey	2010-11-19
*	Document DOT output of universe graph	glondu	2010-11-02
*	update CHANGES w.r.t. extraction	letouzey	2010-10-08
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
*	Update CHANGES: Local/Global Set/Unset.	aspiwack	2010-09-23
*	Clarified role of Set Boolean Equality Schemes wrt Set Equality Scheme +	herbelin	2010-09-02