]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_paramodulation/paramod.mli
Initial implementation of statuses using objects in place of nested records.
[helm.git] / helm / software / components / ng_paramodulation / paramod.mli
index dd866f8db9ea71870b55bad00f1d1ba5f31b80ac..69299b13fd1d6e1fa2ed70d22ab213822860a0f8 100644 (file)
@@ -1,5 +1,5 @@
 val nparamod : 
-  NRstatus.refiner_status ->
+  #NRstatus.status ->
   NCic.metasenv -> NCic.substitution -> NCic.context -> 
     (NCic.term * NCic.term) -> (NCic.term * NCic.term) list ->
      unit