X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite%2FgrafiteAstPp.ml;h=941f75d9d6dae352574be19861ddc79d1775f2c5;hb=bf0b308923fbe96bdd4bd8ee0f4495958211ab6f;hp=18f14c5ce99aefe1f96c1dcf3fc1e3339b9198d1;hpb=f68f452173a5077c58f93587faad65fcced77223;p=helm.git

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 18f14c5ce..941f75d9d 100644
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -36,7 +36,6 @@ 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"
@@ -99,6 +98,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
       in
       let types = List.rev_map to_ident types in
       sprintf "decompose %s %s%s" (pp_idents types) (opt_string_pp what) (pp_intros_specs (None, names)) 
+  | Demodulate _ -> "demodulate"
   | Discriminate (_, term) -> "discriminate " ^ term_pp term
   | Elim (_, term, using, num, idents) ->
       sprintf "elim " ^ term_pp term ^