coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"	Lionel Rieg	2015-06-26
\|
*	Add a [Redirect] vernacular command	Clément Pit--Claudel	2015-05-04
\| \| \| \| \| \| \|	The command [Redirect "filename" (...)] redirects all the output of [(...)] to file "filename.out". This is useful for storing the results of an [Eval compute], for redirecting the results of a large search, for automatically generating traces of interesting developments, and so on.
*	Fix some typos.	Guillaume Melquiond	2015-04-02
\|
*	Putting the From parameter of the Require command into the AST.	Pierre-Marie Pédrot	2015-03-27
\|
*	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Proof using: New vernacular to name sets of section variables	Enrico Tassi	2014-12-18
\|
*	Add additional location information to AST XMLs.	Carst Tankink	2014-10-01
\|
*	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin	2014-09-30
\| \| \| \| \| \| \| \|	will name the goal id; writing ?[?id] will use the first fresh name available based with prefix id. Tactics intro, rename, change, ... from logic.ml now preserve goal name; cut preserves goal name on its main premise.
*	XML pretty printing for AST (work by François Poulain, project DoCoq)	Enrico Tassi	2014-09-29
	It is not 100% complete, but the main part is there.