X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAstPp.ml;h=52f7b1ab20099709575e37bcbd18eb61f2b96116;hb=cb7af66937e8c72ae6ea6694350a0c86f3e6ccf9;hp=86d10c87730294bf0db4e097c4ec442dec47f3e4;hpb=1416af941615fa434b71c0adda461d5bcac65f89;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index 86d10c877..52f7b1ab2 100644
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -71,7 +71,7 @@ let rec pp_tactic = function
   | Cut (_, term) -> "cut " ^ pp_term_ast term
   | Decompose (_, ident, principles) ->
       sprintf "decompose %s %s" (pp_idents principles) ident
-  | Discriminate (_, ident) -> "discriminate " ^ ident
+  | Discriminate (_, term) -> "discriminate " ^ pp_term_ast term
   | Elim (_, term, using) ->
       sprintf "elim " ^ pp_term_ast term ^
       (match using with None -> "" | Some term -> " using " ^ pp_term_ast term)