diff options
| author | Emilio Jesus Gallego Arias | 2018-11-14 19:42:30 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-17 17:11:51 +0100 |
| commit | c8b6081ebacc0dd8ee1527a271a380dbd3b859b9 (patch) | |
| tree | 622a359d4d1bc57b104ad042a9b1fc5e5d8d11fd /plugins/setoid_ring | |
| parent | 71938f0de10e1f3b69b1158b80b4898bf3a7dfdb (diff) | |
[vernacextend] Consolidate extension points API
We group the extension API and datatypes under `Vernacextend`.
This means that the base plugin dependency is now `coq.vernac` from
`coq.stm`.
This is quite important as for example the LSP server won't like to
link the STM in.
LTAC still depends on the STM by means of the ltac_profile part tho.
The next step could be to move the extension point below `Vernacexpr`.
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/g_newring.mlg | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/setoid_ring/g_newring.mlg b/plugins/setoid_ring/g_newring.mlg index 3ddea7eb30..f59ca4cef4 100644 --- a/plugins/setoid_ring/g_newring.mlg +++ b/plugins/setoid_ring/g_newring.mlg @@ -86,7 +86,7 @@ END VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods_opt(l) ] -> { let l = match l with None -> [] | Some l -> l in add_theory id t l } - | [ "Print" "Rings" ] => {Vernac_classifier.classify_as_query} -> { + | [ "Print" "Rings" ] => { Vernacextend.classify_as_query } -> { Feedback.msg_notice (strbrk "The following ring structures have been declared:"); Spmap.iter (fun fn fi -> let sigma, env = Pfedit.get_current_context () in @@ -130,7 +130,7 @@ END VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF | [ "Add" "Field" ident(id) ":" constr(t) field_mods_opt(l) ] -> { let l = match l with None -> [] | Some l -> l in add_field_theory id t l } -| [ "Print" "Fields" ] => {Vernac_classifier.classify_as_query} -> { +| [ "Print" "Fields" ] => {Vernacextend.classify_as_query} -> { Feedback.msg_notice (strbrk "The following field structures have been declared:"); Spmap.iter (fun fn fi -> let sigma, env = Pfedit.get_current_context () in |