coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	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...
*	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.
*	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.