X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=652f10b2ad3217d2a30c532af134daf1728ccc4a;hb=f5b9e1d5511a13ca5bb424c149781087aa0c8e31;hp=c4eacfb5a36d18940f4b04050339e0ffe8e4a484;hpb=8344b3062fc040a7565e43b646d12197d1d51ee3;p=helm.git

diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml
index c4eacfb5a..652f10b2a 100644
--- a/matita/components/grafite/grafiteAstPp.ml
+++ b/matita/components/grafite/grafiteAstPp.ml
@@ -168,8 +168,11 @@ let pp_ncommand status = function
   | NInverter (_,_,_,_,_)
   | NUnivConstraint (_) -> "not supported"
   | NCoercion (_) -> "not supported"
-  | NObj (_,obj) -> NotationPp.pp_obj (NotationPp.pp_term status) obj
-  | NQed (_) -> "qed"
+  | 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 "