New command "inverter" used to generate an induction/inversion principle for

[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 4e10cfa8b28e3187af114b1642443851aced8b26..0fddb21639496a2085b480598c752d6d3099b003 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -332,6 +332,8 @@ let pp_command ~term_pp ~obj_pp = function
      pp_coercion ~term_pp t do_composites i j
   | PreferCoercion (_,t) -> 
      "prefer coercion " ^ term_pp t
+  | Inverter (_,n,ty,params) ->
+     "inverter " ^ n ^ " for " ^ term_pp ty ^ " " ^ List.fold_left (fun acc x -> acc ^ (match x with true -> "%" | _ -> "?")) "" params
   | UnificationHint (_,t, n) -> 
       "unification hint " ^ string_of_int n ^ " " ^ term_pp t
   | Default (_,what,uris) -> pp_default what uris