X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fsaturate_main.ml;h=758437b76c7f925e13f412c1e612e96c13ce56a8;hb=a423d321a98c6f31dab56505fe7acf0110df38e8;hp=14d81569aab72dd96fe2f512cb9aa82c737a553c;hpb=4dd2d3dc8e1dbb22d71c8fa741a20fb7d506930a;p=helm.git

diff --git a/helm/ocaml/paramodulation/saturate_main.ml b/helm/ocaml/paramodulation/saturate_main.ml
index 14d81569a..758437b76 100644
--- a/helm/ocaml/paramodulation/saturate_main.ml
+++ b/helm/ocaml/paramodulation/saturate_main.ml
@@ -100,6 +100,7 @@ let _ =
     | "lpo" -> Utils.compare_terms := Utils.lpo
     | "kbo" -> Utils.compare_terms := Utils.kbo
     | "nr-kbo" -> Utils.compare_terms := Utils.nonrec_kbo
+    | "ao" -> Utils.compare_terms := Utils.ao
     | o -> raise (Arg.Bad ("Unknown term ordering: " ^ o))
   and set_fullred b = S.use_fullred := b
   and set_time_limit v = S.time_limit := float_of_int v