X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;fp=matitaB%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=62ffc2762949057082502d3fd1cbe1b9300078f6;hb=928af763320668168206e88d93e8a77698f3b925;hp=d4d312bd2b455c38489f81c50ee53e046f1cfd0f;hpb=c9c6cae5121a25b05450ea42578f14f74569cfbf;p=helm.git

diff --git a/matitaB/components/grafite/grafiteAstPp.ml b/matitaB/components/grafite/grafiteAstPp.ml
index d4d312bd2..62ffc2762 100644
--- a/matitaB/components/grafite/grafiteAstPp.ml
+++ b/matitaB/components/grafite/grafiteAstPp.ml
@@ -54,7 +54,7 @@ let pp_tactic_pattern status ~map_unicode_to_tex (what, hyp, goal) =
 let rec pp_ntactic status ~map_unicode_to_tex =
  let pp_tactic_pattern = pp_tactic_pattern ~map_unicode_to_tex in
  function
-  | NApply (_,t) -> "napply " ^ NotationPp.pp_term status t
+  | NApply (_,t) -> "@" ^ NotationPp.pp_term status t
   | NSmartApply (_,t) -> "fixme"
   | NAuto (_,(None,flgs)) ->
       "nautobatch" ^
@@ -166,8 +166,11 @@ let pp_ncommand status = function
   | NInverter (_,_,_,_,_)
   | NUnivConstraint (_) -> "not supported"
   | NCoercion (_) -> "not supported"
-  | NObj (_,obj) -> NotationPp.pp_obj (NotationPp.pp_term status) obj
-  | NQed (_,_) -> "nqed"
+  | NObj (_,obj,index) -> 
+      (if not index then "-" else "") ^ 
+        NotationPp.pp_obj (NotationPp.pp_term status) obj
+  | NQed (_,true) -> "qed"
+  | NQed (_,false) -> "qed-"
   | NCopy (_,name,uri,map) -> 
       "copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^ 
         String.concat " and " 
@@ -176,9 +179,9 @@ let pp_ncommand status = function
             map)
   | Include (_,mode,path) -> (* not precise, since path is absolute *)
       if mode = WithPreferences then
-        "include \"" ^ path ^ "\"."
+        "include \"" ^ path ^ "\""
       else
-        "include' \"" ^ path ^ "\"."
+        "include' \"" ^ path ^ "\""
   | Alias (_,s) -> pp_alias s
   | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) ->
       pp_interpretation dsc symbol arg_patterns cic_appl_pattern