coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[vernac] use a record for the contents of the “deprecated” attribute	Vincent Laporte	2018-07-03
\|
*	[vernac] Add a “deprecated” attribute	Vincent Laporte	2018-07-03
\|
*	[vernac] mk_atts: an atts record with default values	Vincent Laporte	2018-07-03
\|
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	[vernac] adds the “program” flag to the “atts” record	Vincent Laporte	2017-12-29
\|
*	[vernac] Add polymorphic to the type of vernac interpration options.	Emilio Jesus Gallego Arias	2017-11-27
\|
*	[vernac] Start to uniformize type of vernac interpretation.	Emilio Jesus Gallego Arias	2017-11-27
\| \| \| \| \| \| \| \|	In particular, we put all the context in the atts structure, and generalize the type of the parameters of a vernac. I hope this helps people working on "attributes", my motivation is indeed having a more robust interpretation.
*	[plugin] Encapsulate modifiers to vernac commands.	Emilio Jesus Gallego Arias	2017-11-22
\| \| \| \| \| \| \|	This is a continuation on #6183 and another step towards a more functional interpretation of commands. In particular, this should allow us to remove the locality hack.
*	[plugins] Prepare plugin API for functional handling of state.	Emilio Jesus Gallego Arias	2017-11-19
\| \| \| \| \| \| \| \|	To this purpose we allow plugins to register functions that will modify the state. This is not used yet, but will be used soon when we remove the global handling of the proof state.
*	provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rules	Matej Košík	2017-11-01
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Originally, it was not possible to define a new vernacular command in the following way: VERNAC COMMAND EXTEND Cmd6 CLASSIFIED AS QUERY [ "SomeCmd" ] -> [ Feedback.msg_notice ?loc (Pp.str "some message") ] END because "loc : Loc.t" was not bound. This commit fixes that, i.e. the location of the custom Vernacular command (within *.v file) is made available as "loc" variable bound on the right side of "->" .
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	[stm] Break stm/toplevel dependency loop.	Emilio Jesus Gallego Arias	2017-02-15
	Currently, the STM, vernac interpretation, and the toplevel are intertwined in a mutual dependency that needs to be resolved using imperative callbacks. This is problematic for a few reasons, in particular it makes the interpretation of commands that affect the document quite intricate. As a first step, we split the `toplevel/` directory into two: "pure" vernac interpretation is moved to the `vernac/` directory, on which the STM relies. Test suite passes, and only one command seems to be disabled with this approach, "Show Script" which is to my understanding obsolete. Subsequent commits will fix this and refine some of the invariants that are not needed anymore.