X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FgrafiteAstPp.ml;h=6af1efd714406afea6c87e2bf0d37af966b402ae;hb=1bcad789810fd37d346e690f18557aeedc6fe08c;hp=029152e36fdfe6eac95bfd41e51c9df323964c1d;hpb=2817260358878e72fa359c6d2431b4c7c358a841;p=helm.git

diff --git a/helm/ocaml/cic_notation/grafiteAstPp.ml b/helm/ocaml/cic_notation/grafiteAstPp.ml
index 029152e36..6af1efd71 100644
--- a/helm/ocaml/cic_notation/grafiteAstPp.ml
+++ b/helm/ocaml/cic_notation/grafiteAstPp.ml
@@ -78,8 +78,15 @@ let rec pp_tactic = function
      "cut " ^ pp_term_ast term ^
       (match ident with None -> "" | Some id -> " as " ^ id)
   | DecideEquality _ -> "decide equality"
-  | Decompose (_, term) ->
-      sprintf "decompose %s" (pp_term_ast term)
+  | Decompose (_, [], what, names) ->
+      sprintf "decompose %s%s" 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) what (pp_intros_specs (None, names)) 
   | Discriminate (_, term) -> "discriminate " ^ pp_term_ast term
   | Elim (_, term, using, num, idents) ->
       sprintf "elim " ^ pp_term_ast term ^