X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAst2Box.ml;h=f43091c755a012cd059cfd64d52c289151013e06;hb=cb7af66937e8c72ae6ea6694350a0c86f3e6ccf9;hp=35a27ff24785fa17640b023ebc5d374efd95a076;hpb=e32693f30563379989b75b53c3be088396b732da;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml
index 35a27ff24..f43091c75 100644
--- 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