]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_paramodulation/nCicParamod.mli
Exported forward_inference_step
[helm.git] / helm / software / components / ng_paramodulation / nCicParamod.mli
index d24e5b57f0ee94abf77f2346647d1987a08bb534..067235158043fda321e20fecebe08a458ffc8f12 100644 (file)
@@ -11,6 +11,9 @@
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
+module NCicParamod(C : NCicBlob.NCicContext) : Paramod.Paramod
+with type t = NCic.term and type input = NCic.term 
+
 val nparamod :
   #NRstatus.status ->
   NCic.metasenv -> NCic.substitution -> NCic.context ->