The discriminate tactic accepts a term, not only an identifier!

[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 86d10c87730294bf0db4e097c4ec442dec47f3e4..52f7b1ab20099709575e37bcbd18eb61f2b96116 100644 (file)
--- 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)