X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Flibrary%2FcoercGraph.mli;h=1923a964a7fa8e799fe890194232d696c3af34c1;hb=ff4f8bef029d1c55b2e50c5635b0ca98c967d9ff;hp=b21fb96bef067c54effceef08f3ff1f99b1bc11f;hpb=cf3635c0830661f59d16339cd7fc9c3b948fcbc8;p=helm.git

diff --git a/helm/ocaml/library/coercGraph.mli b/helm/ocaml/library/coercGraph.mli
index b21fb96be..1923a964a 100644
--- 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,17 +34,7 @@ type coercion_search_result =
 val look_for_coercion :
   Cic.term -> Cic.term -> coercion_search_result
 
-(* it returns the list of composite coercions                             *)
-(* composite coercions are always declared as such; they are added to the *)
-(* CoercDb adding them to the library is left to the caller               *)
-val add_coercion:
- UriManager.uri -> 
-   (UriManager.uri * Cic.obj) list
-
-val remove_coercion: UriManager.uri -> unit
-
 val is_a_coercion: Cic.term -> bool
 val source_of: Cic.term -> Cic.term
 val target_of: Cic.term -> Cic.term
 
-val remove_all: unit -> unit