coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-01-27	[vernac] move vernac_classifier to vernac	Enrico Tassi

2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2018-11-17	[vernacextend] Consolidate extension points API	Emilio Jesus Gallego Arias
	We group the extension API and datatypes under `Vernacextend`. This means that the base plugin dependency is now `coq.vernac` from `coq.stm`. This is quite important as for example the LSP server won't like to link the STM in. LTAC still depends on the STM by means of the ltac_profile part tho. The next step could be to move the extension point below `Vernacexpr`.
2018-07-12	Export a wrapper simplifying the registration of vernacular commands.	Pierre-Marie Pédrot

2018-05-17	[STM] Nested Proofs Allowed has to be executed immediately	Enrico Tassi
	since it affects scheduling (actually the error the option lets one silence)
2018-02-27	Update headers following #6543.	Théo Zimmermann

2017-12-20	Separate vernac controls and regular commands.	Maxime Dénès
	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.
2017-10-17	[stm] First step to move interpretation of Undo commands out of the classifier.	Emilio Jesus Gallego Arias
	The vernacular classifier has a current special case for "Undo" like commands, as it needs access to the document structure in order to produce the proper "VtBack" classification, however the classifier is defined before the document is. We introduce a new delegation status `VtMeta` that allows us to interpreted such commands outside the classifier itself.
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2016-01-20	Update copyright headers.	Maxime Dénès

2015-01-12	Update headers.	Maxime Dénès

2014-11-09	new: Optimize Proof, Optimize Heap	Enrico Tassi
	- drops all Defined entries from the evar map (applying the subst to the initial evar and the undefined evars types). - call Gc.compact Now the question is: where should these two commands be documented?
2014-09-10	VernacExtend does not dispatch on type anymore.	Pierre-Marie Pédrot

2014-04-25	Adding a stm/ folder, as asked during last workgroup. It was essentially moving	Pierre-Marie Pédrot
	files around. A bunch of files from lib/ that were only used in the STM were moved, as well as part of toplevel/ related to the STM.