aboutsummaryrefslogtreecommitdiff
path: root/stm/vernac_classifier.ml
AgeCommit message (Expand)Author
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
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-21[vernac] Remove stale bool parameter from `VernacStartTheoremProof`Emilio Jesus Gallego Arias
2017-06-20Merge PR#774: [ide] Add route_id parameter to query call.Maxime Dénès
2017-06-18[ide] Add route_id parameter to query call.Emilio Jesus Gallego Arias
2017-06-16Fix bugs and add an option for cumulativityAmin Timany
2017-06-07Merge PR#717: [proof] Deprecate "proof mode" APIMaxime Dénès
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-05-31[proof] Deprecate "proof mode" APIEmilio Jesus Gallego Arias
2017-04-21Remove VernacErrorGaetan Gilbert
2017-04-15Merge branch 'v8.6' into trunkMaxime Dénès
2017-04-14Fix anomaly when doing [all:Check _.] during a proof.Gaetan Gilbert
2017-03-24[stm] Remove some obsolete vernacs/classification.Emilio Jesus Gallego Arias
2016-11-18Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"Maxime Dénès
2016-11-17[stm] Remove STM-related vernacularsEmilio Jesus Gallego Arias
2016-10-01Add command 'Set foo Append "bar"' for appending to an option (bug #5109).Guillaume Melquiond
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-17par: like all: but in parallelEnrico Tassi
2016-06-07DocumentationEnrico Tassi
2016-06-06STM: proof block detection for bullets and { block }Enrico Tassi
2016-06-06STM: proof block detection/error resilience APIEnrico Tassi
2016-05-10Proof_global, STM: cleanup + use default_proof_mode instead of "Classic"Enrico Tassi
2016-03-20Moving the Ltac definition command to an EXTEND based command.Pierre-Marie Pédrot
2016-03-20Moving Tactic Notation to an EXTEND based command.Pierre-Marie Pédrot
2016-03-19Moving VernacSolve to an EXTEND-based definition.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-01Remove useless recursive flags.Guillaume Melquiond
2015-12-18CLEANUP: Vernacexpr.VernacDeclareTacticDefinitionMatej Kosik
2015-12-18CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...Matej Kosik
2015-12-18CLEANUP: Vernacexpr.vernac_exprMatej Kosik
2015-10-08Axioms now support the universe binding syntax.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:50:35 +0000