X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=183fc5ec464ca725ccd4b6b54b591ad326478d70;hb=fa6addea4fa1f37567dca9104164710870a50392;hp=ce9ea017b2c1565d6b82302e75f8d1582188a9b4;hpb=3ce05ecd50428a27ce17adb070620aeeaf2aed65;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index ce9ea017b..183fc5ec4 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -148,8 +148,6 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Reduce (_, kind, pat) ->
       sprintf "%s %s" (pp_reduction_kind kind) (pp_tactic_pattern pat)
   | Reflexivity _ -> "reflexivity"
-  | Rename (_, froms, tos) -> 
-     sprintf "rename %s as %s" (pp_idents froms) (pp_idents tos)
   | Replace (_, pattern, t) ->
       sprintf "replace %s with %s" (pp_tactic_pattern pattern) (lazy_term_pp t)
   | Rewrite (_, pos, t, pattern, names) -> 
@@ -202,8 +200,9 @@ let pp_arg ~term_pp arg =
 let pp_macro ~term_pp = 
   let term_pp = pp_arg ~term_pp in
   let style_pp = function
-     | Declarative -> ""
-     | Procedural -> "procedural "
+     | Declarative         -> ""
+     | Procedural None     -> "procedural "
+     | Procedural (Some i) -> sprintf "procedural %u " i
   in
   let prefix_pp prefix = 
      if prefix = "" then "" else sprintf " \"%s\"" prefix