removed first Cic.term from type equality, added an int (weight of the equality)

[helm.git] / helm / ocaml / paramodulation / inference.mli

diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli
index 74194e84a0f7aa678d36708d555299a86ef99ef8..aa2b9231d09cc6a609da724743c49858ab6b2e37 100644 (file)
--- a/helm/ocaml/paramodulation/inference.mli
+++ b/helm/ocaml/paramodulation/inference.mli
@@ -1,5 +1,5 @@
 type equality =
-    Cic.term *           (* proof *)
+    int *                (* weight *)
     (Cic.term *          (* type *)
      Cic.term *          (* left side *)
      Cic.term *          (* right side *)
@@ -66,7 +66,7 @@ val equality_of_term: ?eq_uri:UriManager.uri -> Cic.term -> Cic.term ->
    returns a list of new clauses inferred with a left superposition step
    the negative equation "target" and the positive equation "source"
 *)
-val superposition_left: environment -> equality -> equality -> equality list
+(* val superposition_left: environment -> equality -> equality -> equality list *)
 
 (**
    superposition_right newmeta env target source
@@ -75,10 +75,10 @@ val superposition_left: environment -> equality -> equality -> equality list
    "newmeta" is the first free meta index, i.e. the first number above the
    highest meta index: its updated value is also returned
 *)
-val superposition_right:
-  int -> environment -> equality -> equality -> int * equality list
+(* val superposition_right: *)
+(*   int -> environment -> equality -> equality -> int * equality list *)
 
-val demodulation: int -> environment -> equality -> equality -> int * equality
+(* val demodulation: int -> environment -> equality -> equality -> int * equality *)
 
 val meta_convertibility_eq: equality -> equality -> bool
 
@@ -86,7 +86,7 @@ val is_identity: environment -> equality -> bool
 
 val string_of_equality: ?env:environment -> equality -> string
 
-val subsumption: environment -> equality -> equality -> bool
+(* val subsumption: environment -> equality -> equality -> bool *)
 
 val metas_of_term: Cic.term -> int list