aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/vernac_classifier.ml
Commit message (Expand)AuthorAge
* [vernac] mk_atts: an atts record with default valuesGravatar Vincent Laporte2018-07-03
* [vernac] attribute_of_flagsGravatar Vincent Laporte2018-07-03
* [STM] Nested Proofs Allowed has to be executed immediatelyGravatar Enrico Tassi2018-05-17
* Merge PR #7139: [stm] More cleanup of "classification is not an interpreter"Gravatar Enrico Tassi2018-04-05
|\
* \ Merge PR #7138: [stm] Move VernacBacktrack to the toplevel.Gravatar Enrico Tassi2018-04-04
|\ \
| | * [stm] More cleanup of "classification is not an interpreter"Gravatar Emilio Jesus Gallego Arias2018-04-01
| |/
| * [stm] Move VernacBacktrack to the toplevel.Gravatar Emilio Jesus Gallego Arias2018-04-01
* | Remove deprecated commands Arguments Scope and Implicit ArgumentsGravatar Jasper Hugunin2018-03-30
|/
* [vernac] Move `Quit` and `Drop` to the toplevel layer.Gravatar Emilio Jesus Gallego Arias2018-03-11
* Implement the Export Set/Unset feature.Gravatar Pierre-Marie Pédrot2018-03-09
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* [vernac] Mutual theorems (VernacStartTheoremProof) always have namesGravatar Vincent Laporte2018-02-01
* [vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionGravatar Vincent Laporte2018-02-01
* [vernac] vernac_expr no longer recursiveGravatar Vincent Laporte2018-01-08
* [flags] Move global time flag into an attribute.Gravatar Emilio Jesus Gallego Arias2017-12-23
* Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-20
* [stm] Remove all but one use of VtUnknown.Gravatar Emilio Jesus Gallego Arias2017-12-09
* Remove "obsolete_locality" and fix STM vernac classification.Gravatar Maxime Dénès2017-11-29
* [stm] Remove VtBack from public classification.Gravatar Emilio Jesus Gallego Arias2017-10-17
* [stm] First step to move interpretation of Undo commands out of the classifier.Gravatar Emilio Jesus Gallego Arias2017-10-17
* Remove STM vernaculars.Gravatar Maxime Dénès2017-09-19
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* [vernac] Remove stale bool parameter from `VernacStartTheoremProof`Gravatar Emilio Jesus Gallego Arias2017-06-21
* Merge PR#774: [ide] Add route_id parameter to query call.Gravatar Maxime Dénès2017-06-20
|\
| * [ide] Add route_id parameter to query call.Gravatar Emilio Jesus Gallego Arias2017-06-18
* | Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
|/
* Merge PR#717: [proof] Deprecate "proof mode" APIGravatar Maxime Dénès2017-06-07
|\
* | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| * [proof] Deprecate "proof mode" APIGravatar Emilio Jesus Gallego Arias2017-05-31
|/
* Remove VernacErrorGravatar Gaetan Gilbert2017-04-21
* Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
|\
| * Fix anomaly when doing [all:Check _.] during a proof.Gravatar Gaetan Gilbert2017-04-14
* | [stm] Remove some obsolete vernacs/classification.Gravatar Emilio Jesus Gallego Arias2017-03-24
| * Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"Gravatar Maxime Dénès2016-11-18
| * [stm] Remove STM-related vernacularsGravatar Emilio Jesus Gallego Arias2016-11-17
|/
* Add command 'Set foo Append "bar"' for appending to an option (bug #5109).Gravatar Guillaume Melquiond2016-10-01
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* par: like all: but in parallelGravatar Enrico Tassi2016-06-17
* DocumentationGravatar Enrico Tassi2016-06-07
* STM: proof block detection for bullets and { block }Gravatar Enrico Tassi2016-06-06
* STM: proof block detection/error resilience APIGravatar Enrico Tassi2016-06-06
* Proof_global, STM: cleanup + use default_proof_mode instead of "Classic"Gravatar Enrico Tassi2016-05-10
* Moving the Ltac definition command to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* Moving Tactic Notation to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* Moving VernacSolve to an EXTEND-based definition.Gravatar Pierre-Marie Pédrot2016-03-19
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Remove useless recursive flags.Gravatar Guillaume Melquiond2016-01-01
* | CLEANUP: Vernacexpr.VernacDeclareTacticDefinitionGravatar Matej Kosik2015-12-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-08 08:53:12 +0000