diff options
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/g_newring.mlg | 62 |
1 files changed, 36 insertions, 26 deletions
diff --git a/plugins/setoid_ring/g_newring.mlg b/plugins/setoid_ring/g_newring.mlg index f59ca4cef4..6be556b2ae 100644 --- a/plugins/setoid_ring/g_newring.mlg +++ b/plugins/setoid_ring/g_newring.mlg @@ -38,24 +38,24 @@ END open Pptactic open Ppconstr -let pr_ring_mod = function - | Ring_kind (Computational eq_test) -> str "decidable" ++ pr_arg pr_constr_expr eq_test +let pr_ring_mod env sigma = function + | Ring_kind (Computational eq_test) -> str "decidable" ++ pr_arg (pr_constr_expr env sigma) eq_test | Ring_kind Abstract -> str "abstract" - | Ring_kind (Morphism morph) -> str "morphism" ++ pr_arg pr_constr_expr morph - | Const_tac (CstTac cst_tac) -> str "constants" ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]" + | Ring_kind (Morphism morph) -> str "morphism" ++ pr_arg (pr_constr_expr env sigma) morph + | Const_tac (CstTac cst_tac) -> str "constants" ++ spc () ++ str "[" ++ pr_raw_tactic env sigma cst_tac ++ str "]" | Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]" - | Pre_tac t -> str "preprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]" - | Post_tac t -> str "postprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]" - | Setoid(sth,ext) -> str "setoid" ++ pr_arg pr_constr_expr sth ++ pr_arg pr_constr_expr ext - | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]" - | Pow_spec(CstTac cst_tac,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]" - | Sign_spec t -> str "sign" ++ pr_arg pr_constr_expr t - | Div_spec t -> str "div" ++ pr_arg pr_constr_expr t + | Pre_tac t -> str "preprocess" ++ spc () ++ str "[" ++ pr_raw_tactic env sigma t ++ str "]" + | Post_tac t -> str "postprocess" ++ spc () ++ str "[" ++ pr_raw_tactic env sigma t ++ str "]" + | Setoid(sth,ext) -> str "setoid" ++ pr_arg (pr_constr_expr env sigma) sth ++ pr_arg (pr_constr_expr env sigma) ext + | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg (pr_constr_expr env sigma) spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]" + | Pow_spec(CstTac cst_tac,spec) -> str "power_tac" ++ pr_arg (pr_constr_expr env sigma) spec ++ spc () ++ str "[" ++ pr_raw_tactic env sigma cst_tac ++ str "]" + | Sign_spec t -> str "sign" ++ pr_arg (pr_constr_expr env sigma) t + | Div_spec t -> str "div" ++ pr_arg (pr_constr_expr env sigma) t } VERNAC ARGUMENT EXTEND ring_mod - PRINTED BY { pr_ring_mod } + PRINTED BY { pr_ring_mod env sigma } | [ "decidable" constr(eq_test) ] -> { Ring_kind(Computational eq_test) } | [ "abstract" ] -> { Ring_kind Abstract } | [ "morphism" constr(morph) ] -> { Ring_kind(Morphism morph) } @@ -74,27 +74,32 @@ END { -let pr_ring_mods l = surround (prlist_with_sep pr_comma pr_ring_mod l) +let pr_ring_mods env sigma l = surround (prlist_with_sep pr_comma (pr_ring_mod env sigma) l) } VERNAC ARGUMENT EXTEND ring_mods - PRINTED BY { pr_ring_mods } + PRINTED BY { pr_ring_mods env sigma } | [ "(" ne_ring_mod_list_sep(mods, ",") ")" ] -> { mods } 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" ] => { Vernacextend.classify_as_query } -> { + | ![proof] [ "Print" "Rings" ] => { Vernacextend.classify_as_query } -> { + fun ~pstate -> Feedback.msg_notice (strbrk "The following ring structures have been declared:"); Spmap.iter (fun fn fi -> - let sigma, env = Pfedit.get_current_context () in + (* We should use the global env here as this shouldn't contain proof + data, however preserving behavior as requested in review. *) + let sigma, env = Option.cata Pfedit.get_current_context + (let e = Global.env () in Evd.from_env e, e) pstate in Feedback.msg_notice (hov 2 (Ppconstr.pr_id (Libnames.basename fn)++spc()++ str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++ str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req)) - ) !from_name } + ) !from_name; + pstate } END TACTIC EXTEND ring_lookup @@ -104,41 +109,46 @@ END { -let pr_field_mod = function - | Ring_mod m -> pr_ring_mod m - | Inject inj -> str "completeness" ++ pr_arg pr_constr_expr inj +let pr_field_mod env sigma = function + | Ring_mod m -> pr_ring_mod env sigma m + | Inject inj -> str "completeness" ++ pr_arg (pr_constr_expr env sigma) inj } VERNAC ARGUMENT EXTEND field_mod - PRINTED BY { pr_field_mod } + PRINTED BY { pr_field_mod env sigma } | [ ring_mod(m) ] -> { Ring_mod m } | [ "completeness" constr(inj) ] -> { Inject inj } END { -let pr_field_mods l = surround (prlist_with_sep pr_comma pr_field_mod l) +let pr_field_mods env sigma l = surround (prlist_with_sep pr_comma (pr_field_mod env sigma) l) } VERNAC ARGUMENT EXTEND field_mods - PRINTED BY { pr_field_mods } + PRINTED BY { pr_field_mods env sigma } | [ "(" ne_field_mod_list_sep(mods, ",") ")" ] -> { mods } 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" ] => {Vernacextend.classify_as_query} -> { +| ![proof] [ "Print" "Fields" ] => {Vernacextend.classify_as_query} -> { + fun ~pstate -> Feedback.msg_notice (strbrk "The following field structures have been declared:"); Spmap.iter (fun fn fi -> - let sigma, env = Pfedit.get_current_context () in + (* We should use the global env here as this shouldn't + contain proof data. *) + let sigma, env = Option.cata Pfedit.get_current_context + (let e = Global.env () in Evd.from_env e, e) pstate in Feedback.msg_notice (hov 2 (Ppconstr.pr_id (Libnames.basename fn)++spc()++ str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++ str"and equivalence relation "++ pr_constr_env env sigma fi.field_req)) - ) !field_from_name } + ) !field_from_name; + pstate } END TACTIC EXTEND field_lookup |