Release 0.5.9.

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

diff --git a/helm/software/components/ng_paramodulation/nCicParamod.mli b/helm/software/components/ng_paramodulation/nCicParamod.mli
index 96eeb71aeda6d8eb2fbfb13e8c1fc017c044702e..067235158043fda321e20fecebe08a458ffc8f12 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicParamod.mli
+++ b/helm/software/components/ng_paramodulation/nCicParamod.mli
@@ -11,33 +11,11 @@
 
 (* $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 -> 
     (NCic.term * NCic.term) -> (NCic.term * NCic.term) list ->
-     (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list
-
-type state 
-val empty_state: state
-val forward_infer_step: state -> NCic.term -> NCic.term -> state
-val index_obj: state -> NUri.uri -> state
-val is_equation: NCic.metasenv ->
-           NCic.substitution -> NCic.context -> NCic.term -> bool
-val paramod : 
-  #NRstatus.status ->
-  NCic.metasenv -> NCic.substitution -> NCic.context ->
-  state -> 
-  (NCic.term * NCic.term) -> 
-  (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list
-val fast_eq_check : 
-  #NRstatus.status ->
-  NCic.metasenv -> NCic.substitution -> NCic.context ->
-  state -> 
-  (NCic.term * NCic.term) -> 
-  (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list
-val demod : 
-  #NRstatus.status ->
-  NCic.metasenv -> NCic.substitution -> NCic.context ->
-  state -> 
-  (NCic.term * NCic.term) -> 
-  (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list
+     (NCic.term * NCic.metasenv * NCic.substitution) list