snapshot

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

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 3ab738ab789a579cc41611e42e15bc90f43d22e4..347eab2dabee8871f938172b44b6da856fc3ef3b 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -91,9 +91,13 @@ let pp_just ~term_pp =
 
 let pp_ntactic ~map_unicode_to_tex = function
   | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
-  | NChange (_,what,wwhat) -> "nchange " ^ CicNotationPp.pp_term what 
-      ^ " " ^ CicNotationPp.pp_term wwhat
+  | NCase1 (_,n) -> "*" ^ n ^ ":"
+  | NChange (_,what,wwhat) -> "nchange " ^ assert false ^ 
+      " with " ^ CicNotationPp.pp_term wwhat
+  | NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^
+      assert false ^ " " ^ assert false
   | NId _ -> "nid"
+  | NIntro (_,n) -> "#" ^ n
 ;;
 
 let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =