aboutsummaryrefslogtreecommitdiff
path: root/vernac/vernacentries.mli
AgeCommit message (Expand)Author
2021-02-11Merge PR #13844: [vernac] pass the loc of the whole command to the interp fun...coqbot-app[bot]
2021-02-11[vernac] pass the loc of the whole command to the interp functionEnrico Tassi
2021-02-04Remove deprecated -sprop-cumulative command line argumentGaëtan Gilbert
2020-04-16Make cumulative sprop a typing flag, deprecate command line -sprop-cumulativeGaëtan Gilbert
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-10-07[vernac] Split vernacular translation and interpretation.Emilio Jesus Gallego Arias
2019-08-14[vernac] Refactor common parts of interp_{,delayed}Emilio Jesus Gallego Arias
2019-08-14[vernac] Pass control attributes to interpretation of delayed proofs.Emilio Jesus Gallego Arias
2019-06-27[vernac] Cleanup on interface of VernacentriesEmilio Jesus Gallego Arias
2019-06-26[stm] [vernac] Remove special ?proof parameter from vernac main pathEmilio Jesus Gallego Arias
2019-06-24[lemmas] Turn Lemmas.info into a proper type with constructor.Emilio Jesus Gallego Arias
2019-06-24[lemmas] Reify info for implicits, univ_decls, prepare for rec_thms.Emilio Jesus Gallego Arias
2019-06-20Merge PR #9645: [proof] Remove terminator type, unifying regular and obligati...Pierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-17[proof] drop parameter from terminator typeEmilio Jesus Gallego Arias
2019-06-17[proofs] Store hooks in the proof object.Emilio Jesus Gallego Arias
2019-06-09[proof] Move proofs that have an associated constant to `Lemmas`Emilio Jesus Gallego Arias
2019-06-04VernacExtend produces vernac_interp_phase ADT (old name functional_vernac)Gaëtan Gilbert
2019-06-04Replace ModifyProofStack by CloseProofGaëtan Gilbert
2019-06-04Rename Proof_global.{pstate -> t}Gaëtan Gilbert
2019-06-04Rename Proof_global.{t -> stack}Gaëtan Gilbert
2019-06-04Vernacextend only returns a proof_global.t option, not a vernacstateGaëtan Gilbert
2019-06-04Alternate syntax for ![]: VERNAC EXTEND Foo STATE proofGaëtan Gilbert
2019-06-04coqpp: add new ![] specifiers for structured proof interactionGaëtan Gilbert
2019-04-25[vernac] [ast] Make location info an attribute of vernaculars.Emilio Jesus Gallego Arias
2019-03-27[vernac] [stm] Tweak `with_fail` and hopefully fix the semantics.Emilio Jesus Gallego Arias
2019-03-27[vernac] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-01Move test_mode from Flags to Vernacentries (use point)Gaëtan Gilbert
2019-01-24[STM] explicit handling of parsing statesEnrico Tassi
2018-11-13[vernac] Rename Vernacinterp to Vernacextend and move extension functions there.Emilio Jesus Gallego Arias
2018-11-02Universe Polymorphism is a normal attribute modulo the stm (no Flags)Gaëtan Gilbert
2018-11-02Command driven attributes.Gaëtan Gilbert
2018-11-02{Vernacentries -> Attributes}.attributes_of_flagsGaëtan Gilbert
2018-11-02Move attributes out of vernacinterp to new attributes moduleGaëtan Gilbert
2018-10-15Providing a centralized API for ARGUMENT EXTEND.Pierre-Marie Pédrot
2018-10-02Pass unnamed arguments to ML macros.Pierre-Marie Pédrot
2018-07-12Statically typecheck the VERNAC EXTEND wrapper.Pierre-Marie Pédrot
2018-07-12Export a wrapper simplifying the registration of vernacular commands.Pierre-Marie Pédrot
2018-07-03[vernac] Generic syntax for flags/attributesVincent Laporte
2018-07-03[vernac] attribute_of_flagsVincent Laporte
2018-06-18Remove reference name type.Maxime Dénès
2018-06-12[api] Remove Misctypes.Emilio Jesus Gallego Arias
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-20Separate vernac controls and regular commands.Maxime Dénès
2017-11-27[vernac] Adjust `interp` to pass polymorphic in the attributes.Emilio Jesus Gallego Arias
2017-11-19[plugins] Prepare plugin API for functional handling of state.Emilio Jesus Gallego Arias
2017-10-17[stm] Remove state-handling from Futures.Emilio Jesus Gallego Arias
2017-10-17[stm] Move interpretation state to VernacentriesEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:06:51 +0000