X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FgrafiteAstPp.ml;h=6af1efd714406afea6c87e2bf0d37af966b402ae;hb=158ae2efea344421adeaf861905fe6ffa64b9f8c;hp=b7a62476cf26b05a9c3d52d4a426aadca0604c7b;hpb=cd602bc57c4ceba6188b4cac0dbf5dad8f5df7b6;p=helm.git

diff --git a/helm/ocaml/cic_notation/grafiteAstPp.ml b/helm/ocaml/cic_notation/grafiteAstPp.ml
index b7a62476c..6af1efd71 100644
--- a/helm/ocaml/cic_notation/grafiteAstPp.ml
+++ b/helm/ocaml/cic_notation/grafiteAstPp.ml
@@ -78,8 +78,15 @@ let rec pp_tactic = function
      "cut " ^ pp_term_ast term ^
       (match ident with None -> "" | Some id -> " as " ^ id)
   | DecideEquality _ -> "decide equality"
-  | Decompose (_, term) ->
-      sprintf "decompose %s" (pp_term_ast term)
+  | Decompose (_, [], what, names) ->
+      sprintf "decompose %s%s" what (pp_intros_specs (None, names)) 
+  | Decompose (_, types, what, names) ->
+      let to_ident = function
+         | Ident id -> id
+	 | Type _   -> assert false 
+      in
+      let types = List.rev_map to_ident types in
+      sprintf "decompose %s %s%s" (pp_idents types) what (pp_intros_specs (None, names)) 
   | Discriminate (_, term) -> "discriminate " ^ pp_term_ast term
   | Elim (_, term, using, num, idents) ->
       sprintf "elim " ^ pp_term_ast term ^
@@ -248,14 +255,11 @@ let pp_l1_pattern = CicNotationPp.pp_term
 let pp_l2_pattern = CicNotationPp.pp_term
 
 let pp_associativity = function
-  | Some Gramext.LeftA -> "left associative "
-  | Some Gramext.RightA -> "right associative "
-  | Some Gramext.NonA -> "non associative "
-  | None -> ""
+  | Gramext.LeftA -> "left associative"
+  | Gramext.RightA -> "right associative"
+  | Gramext.NonA -> "non associative"
 
-let pp_precedence = function
-  | Some i -> sprintf "with precedence %d " i
-  | None -> ""
+let pp_precedence i = sprintf "with precedence %d" i
 
 let pp_command = function
   | Include (_,path) -> "include " ^ path
@@ -274,7 +278,7 @@ let pp_command = function
         (String.concat " " (List.map pp_argument_pattern arg_patterns))
         (pp_cic_appl_pattern cic_appl_pattern)
   | Notation (_, l1_pattern, assoc, prec, l2_pattern) ->
-      sprintf "notation \"%s\" %s%sfor %s"
+      sprintf "notation \"%s\" %s %s for %s"
         (pp_l1_pattern l1_pattern)
         (pp_associativity assoc)
         (pp_precedence prec)