X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=3ab738ab789a579cc41611e42e15bc90f43d22e4;hb=bf6f5b964bd4e6c16401a4bfab3c29d6824be22a;hp=9e3ea3b5a91bc8c6f299609d9d400c8b36a90f84;hpb=84e6cbe962c9a534be48542c098d7bb0d90be9a1;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 9e3ea3b5a..3ab738ab7 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -89,6 +89,13 @@ let pp_just ~term_pp =
   | `Auto params -> pp_auto_params ~term_pp params
 ;;
 
+let pp_ntactic ~map_unicode_to_tex = function
+  | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
+  | NChange (_,what,wwhat) -> "nchange " ^ CicNotationPp.pp_term what 
+      ^ " " ^ CicNotationPp.pp_term wwhat
+  | NId _ -> "nid"
+;;
+
 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
@@ -121,9 +128,11 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
   | AutoBatch (_,params) -> "autobatch " ^ 
       pp_auto_params ~term_pp params
   | Assumption _ -> "assumption"
-  | Cases (_, term, pattern, specs) -> Printf.sprintf "cases " ^ term_pp term ^
-      pp_tactic_pattern pattern ^
-      pp_intros_specs "names " specs 
+  | Cases (_, term, pattern, specs) -> 
+      Printf.sprintf "cases %s %s%s" 
+      (term_pp term)
+      (pp_tactic_pattern pattern)
+      (pp_intros_specs "names " specs)
   | Change (_, where, with_what) ->
       Printf.sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what)
   | Clear (_,ids) -> Printf.sprintf "clear %s" (pp_hyps ids)
@@ -315,8 +324,8 @@ let pp_command ~term_pp ~obj_pp = function
      pp_coercion ~term_pp t do_composites i j
   | PreferCoercion (_,t) -> 
      "prefer coercion " ^ term_pp t
-  | UnificationHint (_,t) -> 
-      "unification hint " ^ term_pp t
+  | UnificationHint (_,t, n) -> 
+      "unification hint " ^ string_of_int n ^ " " ^ term_pp t
   | Default (_,what,uris) -> pp_default what uris
   | Drop _ -> "drop"
   | Include (_,path) -> "include \"" ^ path ^ "\""
@@ -335,8 +344,9 @@ let pp_command ~term_pp ~obj_pp = function
        | None -> "")
   | Print (_,s) -> "print " ^ s
   | Set (_, name, value) -> Printf.sprintf "set \"%s\" \"%s\"" name value
+  | NObj (_,o) -> "not supported"
 
-let pp_punctuation_tactical ~term_pp ~lazy_term_pp =
+let pp_punctuation_tactical =
   function
   | Dot _ -> "."
   | Semicolon _ -> ";"
@@ -346,7 +356,7 @@ let pp_punctuation_tactical ~term_pp ~lazy_term_pp =
   | Wildcard _ -> "*:"
   | Merge _ -> "]"
 
-let pp_non_punctuation_tactical ~term_pp ~lazy_term_pp =
+let pp_non_punctuation_tactical =
   function
   | Focus (_, goals) ->
       Printf.sprintf "focus %s" (String.concat " " (List.map string_of_int goals))
@@ -357,13 +367,16 @@ let pp_executable ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp =
   function
   | Macro (_, macro) -> pp_macro ~term_pp ~lazy_term_pp macro ^ "."
   | Tactic (_, Some tac, punct) ->
-      pp_tactic ~map_unicode_to_tex ~lazy_term_pp ~term_pp tac
-      ^ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct
+      pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp tac
+      ^ pp_punctuation_tactical punct
   | Tactic (_, None, punct) ->
-     pp_punctuation_tactical ~lazy_term_pp ~term_pp punct
+     pp_punctuation_tactical punct
+  | NTactic (_,tac, punct) ->
+     pp_ntactic ~map_unicode_to_tex tac
+     ^ pp_punctuation_tactical punct
   | NonPunctuationTactical (_, tac, punct) ->
-     pp_non_punctuation_tactical ~lazy_term_pp ~term_pp tac
-     ^ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct
+     pp_non_punctuation_tactical tac
+     ^ pp_punctuation_tactical punct
   | Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "."
                       
 let pp_comment ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp =