bugfix update in basic_2

[helm.git] / matita / components / grafite / grafiteAstPp.ml

diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml
index c4eacfb5a36d18940f4b04050339e0ffe8e4a484..92944aaebd5b102be15c0ea93f242e74bc40773f 100644 (file)
--- a/matita/components/grafite/grafiteAstPp.ml
+++ b/matita/components/grafite/grafiteAstPp.ml
@@ -83,7 +83,7 @@ let rec pp_ntactic status ~map_unicode_to_tex =
   | NIntro (_,n) -> "#" ^ n
   | NIntros (_,l) -> "#" ^ String.concat " " l
   | NInversion (_,what,where) -> "ninversion " ^ NotationPp.pp_term status what ^
-      assert false ^ " " ^ assert false
+      "...to be implemented..." ^ " " ^ "...to be implemented..."
   | NLApply (_,t) -> "lapply " ^ NotationPp.pp_term status t
   | NRewrite (_,dir,n,where) -> "nrewrite " ^
      (match dir with `LeftToRight -> ">" | `RightToLeft -> "<") ^
@@ -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 "