initial implementation of `ncoercion name : type := body on name : pat to pat`

[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 f05cb9595b9bb9676b8631d8a6a941addb5af81c..2cd7a4f4fcddfee286d115b84ff79c5a18cee9ad 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -119,8 +119,11 @@ let rec pp_ntactic ~map_unicode_to_tex = function
         (String.concat " " (List.map string_of_int l))
   | NUnfocus _ -> "##unfocus"
   | NSkip _ -> "##skip"
-  | NTry (_,tac) -> "ntry (" ^ pp_ntactic ~map_unicode_to_tex tac ^ ")"
+  | NTry (_,tac) -> "ntry " ^ pp_ntactic ~map_unicode_to_tex tac
   | NAssumption _ -> "nassumption"
+  | NBlock (_,l) -> 
+     "(" ^ String.concat " " (List.map (pp_ntactic ~map_unicode_to_tex) l)^ ")"
+  | NRepeat (_,t) -> "nrepeat " ^ pp_ntactic ~map_unicode_to_tex t
 ;;
 
 let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
@@ -357,6 +360,7 @@ let pp_ncommand = function
       "unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t
   | NObj (_,_)
   | NUnivConstraint (_) -> "not supported"
+  | NCoercion (_) -> "not supported"
   | NQed (_) -> "nqed"
     
 let pp_command ~term_pp ~obj_pp = function