matitaGui: some missing cases during disambiguation now treated

[helm.git] / components / grafite / grafiteAstPp.ml

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index ce9ea017b2c1565d6b82302e75f8d1582188a9b4..183fc5ec464ca725ccd4b6b54b591ad326478d70 100644 (file)
--- a/components/grafite/grafiteAstPp.ml
+++ b/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