coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[stm] Move VernacBacktrack to the toplevel.	Emilio Jesus Gallego Arias	2018-04-01
\| \| \| \| \| \|	This command is legacy, equivalent to `EditAt` and only used by Emacs. We move it to the toplevel so we can kill some legacy code and in particular the `part_of_script` hack.
*	Implement the Export Set/Unset feature.	Pierre-Marie Pédrot	2018-03-09
\| \| \| \| \| \| \|	This feature has been asked many times by different people, and allows to have options in a module that are performed when this module is imported. This supersedes the well-numbered cursed PR #313.
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
\| \| \| \| \| \| \| \| \|	We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way.
*	[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.