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 8fbe6b8d1c709b84dc995fd6bb020e3603346927..2cd7a4f4fcddfee286d115b84ff79c5a18cee9ad 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -360,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