X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;fp=matita%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=00789961ce5dd98ebe480ee453f88b2256583b68;hb=185541ccf10a6c4bf69b3db36fdc4ebc09e4cc42;hp=d56e95de0cacafdcc8b4e785edc6b208c126516d;hpb=b6ceb877c05d27705ef163488aee38e60a86886c;p=helm.git

diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml
index d56e95de0..00789961c 100644
--- a/matita/components/grafite/grafiteAstPp.ml
+++ b/matita/components/grafite/grafiteAstPp.ml
@@ -108,6 +108,8 @@ let rec pp_ntactic status ~map_unicode_to_tex =
      "(" ^ String.concat " " (List.map (pp_ntactic status ~map_unicode_to_tex) l)^ ")"
   | NRepeat (_,t) -> "nrepeat " ^ pp_ntactic status ~map_unicode_to_tex t
   | Assume (_, ident, term) -> "assume" ^ ident ^ ":" ^ NotationPp.pp_term status term
+  | Suppose (_,term,ident,term1) -> "suppose" ^ NotationPp.pp_term status term ^ "(" ^ ident ^ ")" ^ (match
+  term1 with None -> "" | Some t -> " that is equivalent to " ^ NotationPp.pp_term status t)
 ;;
 
 let pp_nmacro status = function