aboutsummaryrefslogtreecommitdiff
path: root/stm/vernac_classifier.ml
AgeCommit message (Expand)Author
2021-01-27[vernac] move vernac_classifier to vernacEnrico Tassi
2020-10-16Fixes/enhancements with local definitions in records.Hugo Herbelin
2020-10-09[stm] move par: implementation to vernac/comTactic and stm/partacEnrico Tassi
2020-07-06Primitive persistent arraysMaxime Dénès
2020-06-26[declare] [api] Removal of duplicated type aliases.Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Proof_global` into `Declare`Emilio Jesus Gallego Arias
2020-03-19Make Cumulative, NonCumulative and Private attributes.Théo Zimmermann
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-13Don't duplicate the inductive keyword for each block elt when parsingGaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-13Return of Refine Instance as an attribute.Gaëtan Gilbert
2019-10-07[vernac] Split vernacular translation and interpretation.Emilio Jesus Gallego Arias
2019-08-14[vernac] Refactor Vernacular Control Attributes into a listEmilio Jesus Gallego Arias
2019-07-25Remove deprecated `Backtrack` commandMaxime Dénès
2019-07-23[vernacexpr] Remove duplicate fixpoint record.Emilio Jesus Gallego Arias
2019-07-23[vernacexpr] Refactor fixpoint AST.Emilio Jesus Gallego Arias
2019-06-24[api] [proof] Move `discharge` type to vernac_ast where it is used.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-11STM: encode in static types that vernac_when is only used when VtSideffGaëtan Gilbert
2019-05-21Remove undocumented Instance : ! syntaxGaëtan Gilbert
2019-05-20Remove VtUnknown classificationMaxime Dénès
2019-05-07[Record] Une a record to gather field declaration attributesVincent Laporte
2019-04-25[vernac] [ast] Make location info an attribute of vernaculars.Emilio Jesus Gallego Arias
2019-04-12Unify Set and Unset handling for optionsGaëtan Gilbert
2019-03-30[vernac] Small cleanup to remove assert false.Emilio Jesus Gallego Arias
2019-02-05Make Program a regular attributeMaxime Dénès
2019-02-04Primitive integersMaxime Dénès
2019-01-28[vernac] Fix classification of `Declare Custom Entry`Emilio Jesus Gallego Arias
2019-01-24[STM] explicit handling of parsing statesEnrico Tassi
2019-01-22Distinguish ASTs for Instance and Declare InstanceMaxime Dénès
2019-01-22VernacDeclareClass -> VernacExistingClassMaxime Dénès
2019-01-22VernacDeclareInstances -> VernacExistingInstanceMaxime Dénès
2019-01-11Fix vernac classification of `Fail Instance`Maxime Dénès
2018-12-17Fix classification of Set Default Proof Mode.Gaëtan Gilbert
2018-11-23change vernac_qed_type to have [VtKeep of vernac_keep_as]Gaëtan Gilbert
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2018-11-17[vernacextend] Consolidate extension points APIEmilio Jesus Gallego Arias
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-02Make attributes more general to make defining #[universes(...)] easyGaë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-09-10Adding a command "Declare Scope" and deprecating scope implicit declaration.Hugo Herbelin
2018-07-29Classify "Declare Custom" as VtNow for the stm.Hugo Herbelin
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
2018-07-12Export a wrapper simplifying the registration of vernacular commands.Pierre-Marie Pédrot
2018-07-03[vernac] mk_atts: an atts record with default valuesVincent Laporte
2018-07-03[vernac] attribute_of_flagsVincent Laporte
2018-05-17[STM] Nested Proofs Allowed has to be executed immediatelyEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:21:04 +0000