Fixed the pretty-printing of the Program plugin.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14917 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 25 insertions, 1 deletions

diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index ca1240e5f1..89fbd6ffa4 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -69,7 +69,6 @@ GEXTEND Gram
 
   END
 
-
 type 'a gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a) Genarg.abstract_argument_type
 
 let (wit_subtac_gallina_loc : Genarg.tlevel gallina_loc_argtype),
@@ -164,3 +163,28 @@ VERNAC COMMAND EXTEND Subtac_Show_Preterm
 | [ "Preterm" "of" ident(name) ] -> [ Subtac_obligations.show_term (Some name) ]
 | [ "Preterm" ] -> [ Subtac_obligations.show_term None ]
 END
+
+open Pp
+
+(* Declare a printer for the content of [Program] *)
+let () =
+  let printer _ _ _ expr = Ppvernac.pr_vernac_body (snd expr) in
+  (* should not happen *)
+  let dummy _ _ _ expr = assert false in
+  Pptactic.declare_extra_genarg_pprule
+    (rawwit_subtac_gallina_loc, printer)
+    (globwit_subtac_gallina_loc, dummy)
+    (wit_subtac_gallina_loc, dummy)
+
+(* Declare a printer for the content of Program tactics *)
+let () =
+  let printer _ _ _ = function
+  | None -> mt ()
+  | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic (Global.env ()) tac
+  in
+  (* should not happen *)
+  let dummy _ _ _ expr = assert false in
+  Pptactic.declare_extra_genarg_pprule
+    (rawwit_subtac_withtac, printer)
+    (globwit_subtac_withtac, dummy)
+    (wit_subtac_withtac, dummy)