X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=fd3c444b9d26e009e55b23453949e60bd1df5ebe;hb=bb0074a578a1d4860516964a3717a99a70c0f28c;hp=eb1a18e5ad00d365ba23e3db088b620ece02ceab;hpb=2c80e9d9409119febcab9c08d6e6cad702384169;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index eb1a18e5a..fd3c444b9 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -68,13 +68,14 @@ let pp_intros_specs s = function
    | None, idents     -> Printf.sprintf " %s%s" s (pp_idents idents)
    | Some num, idents -> Printf.sprintf " %s%i %s" s num (pp_idents idents)
 
-let terms_pp ~term_pp terms = String.concat ", " (List.map term_pp terms)
+let pp_terms ~term_pp terms = String.concat ", " (List.map term_pp terms)
 
 let opt_string_pp = function
    | None -> ""
    | Some what -> what ^ " "
 
 let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
+ let pp_terms = pp_terms ~term_pp in
  let pp_tactics = pp_tactics ~map_unicode_to_tex ~term_pp ~lazy_term_pp in
  let pp_reduction_kind = pp_reduction_kind ~term_pp in
  let pp_tactic_pattern =
@@ -127,7 +128,7 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
       (pp_intros_specs "names " (None, names)) 
   | Demodulate _ -> "demodulate"
   | Destruct (_, None) -> "destruct" 
-  | Destruct (_, Some term) -> "destruct " ^ term_pp term
+  | Destruct (_, Some terms) -> "destruct " ^ pp_terms terms
   | Elim (_, what, using, pattern, specs) ->
       Printf.sprintf "elim %s%s %s%s" 
       (term_pp what)
@@ -159,7 +160,7 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
         (if linear then " linear " else "")
 	(match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ")  
         (term_pp term) 
-        (match terms with [] -> "" | _ -> " to " ^ terms_pp ~term_pp terms)
+        (match terms with [] -> "" | _ -> " to " ^ pp_terms terms)
         (match ident_opt with None -> "" | Some ident -> " as " ^ ident)
   | Left _ -> "left"
   | LetIn (_, term, ident) -> 
@@ -264,9 +265,9 @@ let pp_default what uris =
     (String.concat " " (List.map UriManager.string_of_uri uris))
 
 let pp_coercion uri do_composites arity saturations=
-   Printf.sprintf "coercion %s %d %d (* %s *)"
+   Printf.sprintf "coercion %s %d %d %s"
     (UriManager.string_of_uri uri) arity saturations
-    (if do_composites then "compounds" else "no compounds")
+    (if do_composites then "" else "nocomposites")
     
 let pp_command ~term_pp ~obj_pp = function
   | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri