coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Displaying environment and unfolding aliases in "cannot_unify"	herbelin	2013-02-17
*	Revised the strategy for automatic insertion of spaces when printing	herbelin	2012-12-04
*	CHANGES: document the end of states/initial.coq and coqtop.opt	letouzey	2012-08-23
*	Added support for option Local (at module level) in Tactic Notation.	herbelin	2012-08-11
*	Some changes in CHANGES.	herbelin	2012-08-11
*	Cleaning CHANGES consistently with v8.4. Documenting COMPATIBILITY.	herbelin	2012-08-08
*	Document the command Add/Remove Search Blacklist	letouzey	2012-08-03
*	re-sync CHANGES with 8.4	letouzey	2012-08-03
*	The tactic remember now accepts a final eqn:H option (grant wish #2489)	letouzey	2012-07-09
*	induction/destruct : nicer syntax for generating equations (solves #2741)	letouzey	2012-07-09
*	Quick update to CHANGES, mention especially the new parsing of ->	letouzey	2012-07-05
*	CHANGES: mention the end of induction principles for records	letouzey	2012-06-05
*	Some documentation of recent changes concerning interfaces	letouzey	2012-05-29
*	CHANGES: fix a typo + an entry in the wrong section	letouzey	2012-05-23
*	Intuition: temporary(?) restore the unconditional unfolding of not	letouzey	2012-05-15
*	Remove the Dp plugin.	gmelquio	2012-04-17
*	Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).	herbelin	2012-04-15
*	Update CHANGES	herbelin	2012-04-15
*	MSetRBT : implementation of MSets via Red-Black trees	letouzey	2012-04-13
*	CHANGES: adapt after backport of some features to 8.4	letouzey	2012-04-12
*	info_trivial, info_auto, info_eauto, and debug (trivial\|auto)	letouzey	2012-03-30
*	Slight change in the semantics of arguments scopes: scopes can no	herbelin	2012-03-26
*	Module names and constant/inductive names are now in two separate namespaces	letouzey	2012-03-26
*	Documentation of last commit concerning Backtracking	letouzey	2012-03-23
*	More adaptations of pretyping/coercion to Program mode.	msozeau	2012-03-19
*	Fix bugs related to Program integration.	msozeau	2012-03-19
*	Documentation for Grab Existential Variables.	aspiwack	2012-02-07
*	Breakpoints in Ltac debugger: new command "r foo" to jump to the next	herbelin	2012-01-20
*	Added new command "Set Parsing Explicit" for deactivating parsing (and	herbelin	2012-01-20
*	Added the btauto tactic to the documentation.	ppedrot	2012-01-19
*	update CHANGES w.r.t. simpl	gareuselesinge	2011-12-26
*	Cleaning CHANGES file.	herbelin	2011-12-21
*	Notifying removal of accidental unfolding of recursive calls of	herbelin	2011-12-19
*	Coq_makefile: if no -install is provided, install location is set by a Makefi...	pboutill	2011-12-17
*	CHANGES: some more updates	letouzey	2011-12-12
*	Documentation of appcontext	letouzey	2011-11-29
*	Updated CHANGES file wrt to pattern-matching compilation.	herbelin	2011-11-21
*	CHANGES update	pboutill	2011-11-20
*	CoqIdE configuration file won't pollute your home anymore	pboutill	2011-11-20
*	Add support for XDG_DATA_HOME and XDG_DATA_DIRS.	pboutill	2011-11-20
*	Allow "\|_=>_" in "match" in patterns, no more forced enumeration of constructors	letouzey	2011-11-07
*	Fixing Equality.injectable which did not detect an equality without	herbelin	2011-10-22
*	Completing r14538 (Chung-Kil Hur's trick for fast dependently-typed	herbelin	2011-10-11
*	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