paramodulation is no longer a self-alone module

[helm.git] / helm / ocaml / library / coercGraph.mli

diff --git a/helm/ocaml/library/coercGraph.mli b/helm/ocaml/library/coercGraph.mli
index bd562414ee0e457c16240738ed3208c5dd03a521..1923a964a7fa8e799fe890194232d696c3af34c1 100644 (file)
--- a/helm/ocaml/library/coercGraph.mli
+++ b/helm/ocaml/library/coercGraph.mli
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* This module implements the Query interface to the Coercion Graph *)
+
 type coercion_search_result = 
   | SomeCoercion of Cic.term
   | NoCoercion
@@ -32,10 +34,7 @@ type coercion_search_result =
 val look_for_coercion :
   Cic.term -> Cic.term -> coercion_search_result
 
-(* it returns the list of composite coercions and their auxiliary lemmas  *)
-(* composite coercions are always declared as such; they are added to the *)
-(* library only on demand (i.e. not when processing a .moo)               *)
-val add_coercion:
- basedir:string -> add_composites:bool -> UriManager.uri -> UriManager.uri list
+val is_a_coercion: Cic.term -> bool
+val source_of: Cic.term -> Cic.term
+val target_of: Cic.term -> Cic.term
 
-val remove_coercion: UriManager.uri -> unit