Partially restore the suppose tactic

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

diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml
index d56e95de0cacafdcc8b4e785edc6b208c126516d..00789961ce5dd98ebe480ee453f88b2256583b68 100644 (file)
--- 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