diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 22:13:03 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 22:13:03 +0200 |
commit | a89f5a422d565c52e0c536d7aca2b93f5052f248 (patch) | |
tree | ba5c8c23aaaaf6dff31c85ad86757720f270fb67 /plugins/setoid_ring/g_newring.ml4 | |
parent | 653b587d04e6dc1c162586a4e68df69919b6b72b (diff) |
Revert "Adding printers for ring and field commands."
This reverts commit 9df1a3cf26d78df507d0e35c2d9ca987151777be.
Diffstat (limited to 'plugins/setoid_ring/g_newring.ml4')
-rw-r--r-- | plugins/setoid_ring/g_newring.ml4 | 29 |
1 files changed, 0 insertions, 29 deletions
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 092a0cbd8..1ebb6e6b7 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -34,25 +34,7 @@ TACTIC EXTEND closed_term [ Proofview.V82.tactic (closed_term t l) ] END -open Pptactic -open Ppconstr - -let pr_ring_mod = function - | Ring_kind (Computational eq_test) -> str "decidable" ++ pr_arg pr_constr_expr 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 "]" - | Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_reference 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_reference 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 - VERNAC ARGUMENT EXTEND ring_mod - PRINTED BY pr_ring_mod | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational eq_test) ] | [ "abstract" ] -> [ Ring_kind Abstract ] | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism morph) ] @@ -69,10 +51,7 @@ VERNAC ARGUMENT EXTEND ring_mod | [ "div" constr(div_spec) ] -> [ Div_spec div_spec ] END -let pr_ring_mods l = surround (prlist_with_sep pr_comma pr_ring_mod l) - VERNAC ARGUMENT EXTEND ring_mods - PRINTED BY pr_ring_mods | [ "(" ne_ring_mod_list_sep(mods, ",") ")" ] -> [ mods ] END @@ -96,20 +75,12 @@ TACTIC EXTEND ring_lookup [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t] END -let pr_field_mod = function - | Ring_mod m -> pr_ring_mod m - | Inject inj -> str "completeness" ++ pr_arg pr_constr_expr inj - VERNAC ARGUMENT EXTEND field_mod - PRINTED BY pr_field_mod | [ 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) - VERNAC ARGUMENT EXTEND field_mods - PRINTED BY pr_field_mods | [ "(" ne_field_mod_list_sep(mods, ",") ")" ] -> [ mods ] END |