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

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

diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml
index 35a27ff24785fa17640b023ebc5d374efd95a076..f43091c755a012cd059cfd64d52c289151013e06 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst2Box.ml
+++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml
@@ -56,7 +56,7 @@ let rec count_tactic current_size tac =
        List.fold_left
          (fun size s -> size + (String.length s))
          (current_size + 11 + String.length ident) principles
-    | Discriminate (_, ident) -> current_size + 12 + (String.length ident)
+    | Discriminate (_, term) -> countterm (current_size + 12) term
     | Elim (_, term, using) ->
        let size1 = countterm (current_size + 5) term in
          (match using with 
@@ -164,9 +164,8 @@ and big_tactic2box = function
                          Box.V([],principles);
                          Box.Text([],"]")]);
                Box.Text([],ident)])
-  | Discriminate (_, ident) -> 
-      Box.V([],[Box.Text([],"discriminate");
-               Box.Text([],ident)])
+  | Discriminate (_, term) -> 
+      Box.V([],pretty_append [Box.Text([],"discriminate")] term)
   | Elim (_, term, using) ->
       let using =
        (match using with