X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fgrafite%2FgrafiteAstPp.ml;h=8bd5c96f15862677345877c9487e4ce6a96c5501;hb=771ee8b9d122fa963881c876e86f90531bb7434f;hp=6abfa4dd651b3ba0333d53ed99051866427a95fc;hpb=aa0d60227b785da3355b31519ba11cb4fbd2c925;p=helm.git

diff --git a/helm/ocaml/grafite/grafiteAstPp.ml b/helm/ocaml/grafite/grafiteAstPp.ml
index 6abfa4dd6..8bd5c96f1 100644
--- a/helm/ocaml/grafite/grafiteAstPp.ml
+++ b/helm/ocaml/grafite/grafiteAstPp.ml
@@ -36,6 +36,7 @@ let command_terminator = tactical_terminator
 let pp_idents idents = "[" ^ String.concat "; " idents ^ "]"
 
 let pp_reduction_kind ~term_pp = function
+  | `Demodulate -> "demodulate"
   | `Normalize -> "normalize"
   | `Reduce -> "reduce"
   | `Simpl -> "simplify"