First compiling version

[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 9cffd9d2889af4958d8dc8254ce1af33e31dc18d..8376b256ba6adf614c498f9964ee50de4fb46f3d 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.mli
+++ b/helm/software/components/ng_paramodulation/paramod.mli
@@ -21,15 +21,15 @@ module type Paramod =
       | Error of string 
       | Timeout of int * t Terms.bag
     type bag = t Terms.bag * int
-    val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
-    val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
+    val mk_passive : bag -> input * input -> bag * t Terms.clause
+    val mk_goal : bag -> input * input -> bag * t Terms.clause
     val paramod : 
       useage:bool ->
       max_steps:int ->
       ?timeout:float ->
       bag -> 
-      g_passives:t Terms.unit_clause list -> 
-      passives:t Terms.unit_clause list -> szsontology
+      g_passives:t Terms.clause list -> 
+      passives:t Terms.clause list -> szsontology
   end
 
 module Paramod ( B : Orderings.Blob ) : Paramod