the decompose tactic is now working

[helm.git] / helm / ocaml / cic_transformations / tacticAstPp.ml

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index 794e09e708cbf517b418be743b9899e44c3bab62..d8f54a49f55ceefdf9b6eb97c7bfe68d2114d782 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.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 ^