X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite%2FgrafiteAstPp.ml;h=423e68d4f93ce30e5d77e82cb761eeab9fbcaffe;hb=3f38b6dc5e48855b7a2170de5a5ccb30aded766c;hp=d5fbf80343c42a413c718b27fa3bbc93baf1dfaf;hpb=673e954b37f3a23e73208c67267c7e9d31e3916d;p=helm.git

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index d5fbf8034..423e68d4f 100644
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -95,15 +95,8 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Cut (_, ident, term) ->
      "cut " ^ term_pp term ^
       (match ident with None -> "" | Some id -> " as " ^ id)
-  | Decompose (_, [], what, names) ->
-      sprintf "decompose %s%s" (opt_string_pp what) (pp_intros_specs (None, names)) 
-  | Decompose (_, types, what, names) ->
-      let to_ident = function
-         | Ident id -> id
-	 | Type _   -> assert false 
-      in
-      let types = List.rev_map to_ident types in
-      sprintf "decompose %s %s%s" (pp_idents types) (opt_string_pp what) (pp_intros_specs (None, names)) 
+  | Decompose (_, names) ->
+      sprintf "decompose%s" (pp_intros_specs (None, names)) 
   | Demodulate _ -> "demodulate"
   | Destruct (_, term) -> "destruct " ^ term_pp term
   | Elim (_, term, using, num, idents) ->