X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FgrafiteAstPp.ml;h=7d1f8c22e843e53a5c942851e897c35f2be6d083;hb=f981a524748846acc29b76b6e616af110b4ee13d;hp=029152e36fdfe6eac95bfd41e51c9df323964c1d;hpb=2817260358878e72fa359c6d2431b4c7c358a841;p=helm.git

diff --git a/helm/ocaml/cic_notation/grafiteAstPp.ml b/helm/ocaml/cic_notation/grafiteAstPp.ml
index 029152e36..7d1f8c22e 100644
--- a/helm/ocaml/cic_notation/grafiteAstPp.ml
+++ b/helm/ocaml/cic_notation/grafiteAstPp.ml
@@ -39,10 +39,12 @@ let pp_idents idents = "[" ^ String.concat "; " idents ^ "]"
 let pp_terms_ast terms = String.concat ", " (List.map pp_term_ast terms)
 
 let pp_reduction_kind = function
+  | `Normalize -> "normalize"
   | `Reduce -> "reduce"
   | `Simpl -> "simplify"
+  | `Unfold (Some t) -> "unfold " ^ pp_term_ast t
+  | `Unfold None -> "unfold"
   | `Whd -> "whd"
-  | `Normalize -> "normalize"
  
   
 let pp_pattern (t, hyp, goal) = 
@@ -78,8 +80,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 ^
@@ -254,6 +263,11 @@ let pp_associativity = function
 
 let pp_precedence i = sprintf "with precedence %d" i
 
+let pp_dir_opt = function
+  | None -> ""
+  | Some `LeftToRight -> "> "
+  | Some `RightToLeft -> "< "
+
 let pp_command = function
   | Include (_,path) -> "include " ^ path
   | Qed _ -> "qed"
@@ -270,8 +284,9 @@ let pp_command = function
         dsc symbol
         (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 %s for %s"
+  | Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) ->
+      sprintf "notation %s\"%s\" %s %s for %s"
+        (pp_dir_opt dir_opt)
         (pp_l1_pattern l1_pattern)
         (pp_associativity assoc)
         (pp_precedence prec)