Added initial support for inversion principles in Matita NG.

[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 76651753f92cbe6c6232f7b53ab43efc84b654a8..8cb7538ba2ad84dc4b322a3d979f0c2f406d4327 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -371,6 +371,7 @@ let pp_coercion ~term_pp t do_composites arity saturations=
 let pp_ncommand = function
   | UnificationHint (_,t, n) -> 
       "unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t
+  | NInverter (_,_,_)
   | NObj (_,_)
   | NUnivConstraint (_) -> "not supported"
   | NCoercion (_) -> "not supported"