diff options
| author | Pierre-Marie Pédrot | 2018-11-19 19:10:20 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 19:10:20 +0100 |
| commit | ba8e3caa31e464d1007c4ad54e8d70fd70ca3300 (patch) | |
| tree | f19dd19f84fc0c928e95328f98c8b2a8bf365f27 /plugins/setoid_ring | |
| parent | ddbc4215394ecc0845ab29affec2ab27527ee178 (diff) | |
| parent | c8b6081ebacc0dd8ee1527a271a380dbd3b859b9 (diff) | |
Merge PR #9003: [vernacextend] Consolidate extension points API
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 |