Big commit to let Ferruccio try the merge_coercion patch.

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

diff --git a/helm/ocaml/library/coercDb.mli b/helm/ocaml/library/coercDb.mli
index 2d7a11cae0123d31367f18f9b500addc40c85da7..970d2b98a803b5298055f3af7abc771ed575f0ad 100644 (file)
--- a/helm/ocaml/library/coercDb.mli
+++ b/helm/ocaml/library/coercDb.mli
@@ -23,6 +23,10 @@
  * http://cs.unibo.it/helm/.
  *)
 
+
+ (** THIS MODULE SHOULD BE USED ONLY BY CoercGraph **)
+
+
   (** XXX WARNING: non-reentrant *)
 type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term
 exception EqCarrNotImplemented of string Lazy.t
@@ -31,8 +35,6 @@ val eq_carr: coerc_carr -> coerc_carr -> bool
 val coerc_carr_of_term: Cic.term -> coerc_carr
 val name_of_carr: coerc_carr -> string
 
-val use_coercions: bool ref (** initial status is true *)
- 
 val to_list:
   unit -> 
     (coerc_carr * coerc_carr * UriManager.uri) list
@@ -43,6 +45,10 @@ val add_coercion:
 val remove_coercion:
   (coerc_carr * coerc_carr * UriManager.uri -> bool) -> unit
 
-val find_coercion:
+val find_coercion: 
   (coerc_carr * coerc_carr -> bool) -> UriManager.uri list 
     
+val is_a_coercion: UriManager.uri -> bool
+val get_carr: UriManager.uri -> coerc_carr * coerc_carr
+
+