aboutsummaryrefslogtreecommitdiff
path: root/stm/vernac_classifier.ml
AgeCommit message (Expand)Author
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
2018-04-05Merge PR #7139: [stm] More cleanup of "classification is not an interpreter"Enrico Tassi
2018-04-04Merge PR #7138: [stm] Move VernacBacktrack to the toplevel.Enrico Tassi
2018-04-01[stm] More cleanup of "classification is not an interpreter"Emilio Jesus Gallego Arias
2018-04-01[stm] Move VernacBacktrack to the toplevel.Emilio Jesus Gallego Arias
2018-03-30Remove deprecated commands Arguments Scope and Implicit ArgumentsJasper Hugunin
2018-03-11[vernac] Move `Quit` and `Drop` to the toplevel layer.Emilio Jesus Gallego Arias
2018-03-09Implement the Export Set/Unset feature.Pierre-Marie Pédrot
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2018-02-01[vernac] Mutual theorems (VernacStartTheoremProof) always have namesVincent Laporte
2018-02-01[vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionVincent Laporte
2018-01-08[vernac] vernac_expr no longer recursiveVincent Laporte
2017-12-23[flags] Move global time flag into an attribute.Emilio Jesus Gallego Arias
2017-12-20Separate vernac controls and regular commands.Maxime Dénès
2017-12-09[stm] Remove all but one use of VtUnknown.Emilio Jesus Gallego Arias
2017-11-29Remove "obsolete_locality" and fix STM vernac classification.Maxime Dénès
2017-10-17[stm] Remove VtBack from public classification.Emilio Jesus Gallego Arias
2017-10-17[stm] First step to move interpretation of Undo commands out of the classifier.Emilio Jesus Gallego Arias
2017-09-19Remove STM vernaculars.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 11:30:48 +0000