alpha_eq instead of pervasives.compare

[helm.git] / helm / software / components / ng_paramodulation / paramod.mli

diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli
index 1142b03c7ea47cc451abd48bcdfecc5f5e4a4266..367d7939448f269ebedd755cb688cbc887155c9c 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.mli
+++ b/helm/software/components/ng_paramodulation/paramod.mli
@@ -46,6 +46,8 @@ module type Paramod =
       bag -> 
       g_passives:t Terms.unit_clause list -> 
       passives:t Terms.unit_clause list -> szsontology
+    val demod :
+      state -> input* input -> szsontology
     val fast_eq_check :
       state -> input* input -> szsontology
     val nparamod :