Exported forward_inference_step

[helm.git] / helm / software / components / ng_paramodulation / nCicParamod.ml

diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml
index 846a576c7861f9268aada91cc4642b98150d4e72..6096d88dae1bfd358d4593abe95081c40c196594 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicParamod.ml
+++ b/helm/software/components/ng_paramodulation/nCicParamod.ml
@@ -11,19 +11,23 @@
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
+
+module B(C : NCicBlob.NCicContext): Orderings.Blob 
+  with type t = NCic.term and type input = NCic.term 
+  = Orderings.LPO(NCicBlob.NCicBlob(C))
+
+module NCicParamod(C : NCicBlob.NCicContext) = Paramod.Paramod(B(C))
+
 let nparamod rdb metasenv subst context t table =
-  let module C = 
-    struct
+  let module C =
+    struct 
       let metasenv = metasenv
       let subst = subst
-      let context = context
-    end
-  in
-  let module B : Orderings.Blob 
-      with type t = NCic.term and type input = NCic.term 
-    = Orderings.LPO(NCicBlob.NCicBlob(C))
+      let context = context 
+    end 
   in
-  let module P = Paramod.Paramod(B) in
+  let module B = B(C) in
+  let module P = NCicParamod(C) in
   let module Pp = Pp.Pp(B) in
   let bag, maxvar = Terms.empty_bag, 0 in
   let (bag,maxvar), goals =