coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[vernac] vernac_expr no longer recursive	Vincent Laporte	2018-01-08
\|
*	Merge PR #6492: Remove query-in-IDE warning.	Maxime Dénès	2017-12-29
\|\
\| *	Remove query-in-IDE warning.	Maxime Dénès	2017-12-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	I don't understand what is wrong with putting a query in a script running in the IDE. It is typically needed when giving demos, and that sounds like a ligitimate use case. By the way, we do it ourselves every year during the demo at CoqPL...
* \|	[flags] Move global time flag into an attribute.	Emilio Jesus Gallego Arias	2017-12-23
\|/ \| \| \|	One less global flag.
*	Separate vernac controls and regular commands.	Maxime Dénès	2017-12-20
\| \| \| \| \| \| \| \| \| \| \| \|	Virtually all classifications of vernacular commands (the STM classifier, "filtered commands", "navigation commands", etc.) were broken in presence of control vernaculars like Time, Timeout, Fail. Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac Debug in CoqIDE. This change introduces a type separation between vernacular controls and vernacular commands, together with an "under_control" combinator.
*	Remove STM vernaculars.	Maxime Dénès	2017-09-19
\|
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	[stm] Port the toplevel to the STM.	Emilio Jesus Gallego Arias	2017-04-12
	- We clean-up `Vernac` and make it use the STM API. - Now functions in `Vernac` for use in the toplevel and compiler take an starting `Stateid.t`. - Duplicated `Stm.interp` entry point is removed. - The XML protocol call `interp` is disabled.