paramodulation is not a stand alone tactic: doc fixed.

[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 18f14c5ce99aefe1f96c1dcf3fc1e3339b9198d1..b95df8d366d3a3daf5d70a8efeaac7a20c4875e7 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/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 ^
@@ -154,8 +154,8 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Split _ -> "split"
   | Symmetry _ -> "symmetry"
   | Transitivity (_, term) -> "transitivity " ^ term_pp term
-
-let pp_search_kind = function
+  
+  let pp_search_kind = function
   | `Locate -> "locate"
   | `Hint -> "hint"
   | `Match -> "match"