coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-11-20	[stm] [declare] Remove pinfo internals hack.	Emilio Jesus Gallego Arias
	After the previous commit, the stm should correctly pass proof information, thus we make `proof_object` carry it removing a bunch of internal code.
2020-06-26	[declare] Improve logical code order	Emilio Jesus Gallego Arias
	Now that the interface has mostly stabilized, we move code around to respect internal dependency order. This will allow us to start sharing more code in the 4 principal cases, and also paves the way for the full merging of obligations and the removal of the Proof_ending type in favor of stronger type abstraction.
2020-06-26	[declare] Improve organization of proof/constant information.	Emilio Jesus Gallego Arias
	We unify information about constants so it is shared among all the paths [interactive, NI, obligations]. IMHO the current setup looks pretty good, with information split into a per-constant record `CInfo.t` and variables affecting mutual definitions at once, which live in `Info.t`. Main information outside our `Info` record is `opaque`, which is provided at different moments in several cases. There are a few nits regarding interactive proofs, which will go away in the next commits.
2020-06-26	[declare] Move proof information to declare.	Emilio Jesus Gallego Arias
	At this point the record in lemmas was just a stub; next commit will stop exposing the internals of mutual information, and pave the way for the refactoring of `Info.t` handling in the Declare interface.
2020-04-15	[proof] Merge `Proof_global` into `Declare`	Emilio Jesus Gallego Arias
	We place creation and saving of interactive proofs in the same module; this will allow to make `proof_entry` private, improving invariants and control over clients, and to reduce the API [for example next commit will move abstract declaration into this module, removing the exported ad-hoc `build_constant_by_tactic`] Next step will be to unify all the common code in the interactive / non-interactive case; but we need to tweak the handling of obligations first.
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-10-07	[vernac] Split vernacular translation and interpretation.	Emilio Jesus Gallego Arias
	This allows UI clients to implement a different state management strategy with regards to proofs, and in particular to override `Vernacinterp.interp`. This is work in progress towards having a true `VtTactic` which shall not perform any state changes non-functionally, and actually removing the series of `assert false` due to meta-vernacs.
2018-11-13	[vernac] Rename Vernacinterp to Vernacextend and move extension functions there.	Emilio Jesus Gallego Arias
	This PR fixes an issues that was bugging me for some time, namely that `Vernacinterp` really means `Vernacextend`. We thus rename the file and move the associated functions there, which were incorrectly placed in `Vernacentries`. Note the beneficial effects on reducing the `.mli` API.
2018-11-02	Command driven attributes.	Gaëtan Gilbert
	Commands need to request the attributes they use, with the API encouraging them to error on unsupported attributes.
2018-11-02	Move attributes out of vernacinterp to new attributes module	Gaëtan Gilbert

2018-09-13	Add explicit atribute for template polymorphism.	Gaëtan Gilbert

2018-07-03	[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-02-27	Update headers following #6543.	Théo Zimmermann

2017-12-29	[vernac] adds the “program” flag to the “atts” record	Vincent Laporte

2017-11-27	[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
	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.
2017-11-22	[plugin] Encapsulate modifiers to vernac commands.	Emilio Jesus Gallego Arias
	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.
2017-11-19	[plugins] Prepare plugin API for functional handling of state.	Emilio Jesus Gallego Arias
	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.
2017-11-01	provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rules	Matej Košík
	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 "->" .
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2017-02-15	[stm] Break stm/toplevel dependency loop.	Emilio Jesus Gallego Arias
	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.