X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Flibrary%2FcoercDb.mli;h=9e8bf5e9c03066cf219921ac66baaed7a96918d5;hb=ff4f8bef029d1c55b2e50c5635b0ca98c967d9ff;hp=970d2b98a803b5298055f3af7abc771ed575f0ad;hpb=cf3635c0830661f59d16339cd7fc9c3b948fcbc8;p=helm.git

diff --git a/helm/ocaml/library/coercDb.mli b/helm/ocaml/library/coercDb.mli
index 970d2b98a..9e8bf5e9c 100644
--- a/helm/ocaml/library/coercDb.mli
+++ b/helm/ocaml/library/coercDb.mli
@@ -24,7 +24,11 @@
  *)
 
 
- (** THIS MODULE SHOULD BE USED ONLY BY CoercGraph **)
+ (** THIS MODULE SHOULD BE USED ONLY BY CoercGraph/CicCoercion/librarySync
+  * 
+  *   and may be merged with CicCoercion...
+  *  
+  * **)
 
 
   (** XXX WARNING: non-reentrant *)
@@ -51,4 +55,4 @@ val find_coercion:
 val is_a_coercion: UriManager.uri -> bool
 val get_carr: UriManager.uri -> coerc_carr * coerc_carr
 
-
+val term_of_carr: coerc_carr -> Cic.term