coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-08-14	[vernac] Refactor Vernacular Control Attributes into a list	Emilio Jesus Gallego Arias
	We place control attributes on their own, datatype, similarly to regular attributes. This is a step towards fixing #10452 , as we can now decouple control attributes from the vernac AST itself, allowing to pass them independently.
2019-07-25	Remove deprecated `Backtrack` command	Maxime Dénès
	It has been deprecated since 8.4. The documentation was incorrect since at least 8.5 (the last two arguments were ignored). `Backtrack m n p` was a synonym for `BackTo m` We also move `BackTo` handling to coqtop, since it is not meant to be part of the document.
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2019-04-25	[vernac] [ast] Make location info an attribute of vernaculars.	Emilio Jesus Gallego Arias
	This has been a mess for quite a while, we try to improve it.
2019-03-30	[vernac] Small cleanup to remove assert false.	Emilio Jesus Gallego Arias
	This is a fairly small cleanup on the `vernac_interp` function, which makes code cleaner and for example would allow to have `Load` inside `Load`. [Not that we would ever want that]
2018-04-01	[stm] Move VernacBacktrack to the toplevel.	Emilio Jesus Gallego Arias
	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.
2018-03-09	Implement the Export Set/Unset feature.	Pierre-Marie Pédrot
	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.
2018-02-27	Update headers following #6543.	Théo Zimmermann

2018-02-22	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias
	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.
2018-01-08	[vernac] vernac_expr no longer recursive	Vincent Laporte

2017-12-29	Merge PR #6492: Remove query-in-IDE warning.	Maxime Dénès

2017-12-27	Remove query-in-IDE warning.	Maxime Dénès
	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...
2017-12-23	[flags] Move global time flag into an attribute.	Emilio Jesus Gallego Arias
	One less global flag.
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-09-19	Remove STM vernaculars.	Maxime Dénès

2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2017-04-12	[stm] Port the toplevel to the STM.	Emilio Jesus Gallego Arias
	- 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.