Adding printers for ring and field commands.

1 files changed, 29 insertions, 0 deletions

diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 1ebb6e6b7..092a0cbd8 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -34,7 +34,25 @@ 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) ]
@@ -51,7 +69,10 @@ 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
 
@@ -75,12 +96,20 @@ 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