X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcoercDb.mli;h=2d7a11cae0123d31367f18f9b500addc40c85da7;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=1d56132eab2c1a7ce904b73c941508dce5ca29ea;hpb=6376b9d56df8c0151a4cd5f35f2646d9922b5858;p=helm.git

diff --git a/helm/ocaml/cic_unification/coercDb.mli b/helm/ocaml/cic_unification/coercDb.mli
index 1d56132ea..2d7a11cae 100644
--- a/helm/ocaml/cic_unification/coercDb.mli
+++ b/helm/ocaml/cic_unification/coercDb.mli
@@ -22,17 +22,27 @@
  * For details, see the HELM World-Wide-Web page,
  * http://cs.unibo.it/helm/.
  *)
+
+  (** 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
+exception EqCarrOnNonMetaClosed
+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:
+val to_list:
   unit -> 
-    (UriManager.uri * UriManager.uri * UriManager.uri) list
+    (coerc_carr * coerc_carr * UriManager.uri) list
 
 val add_coercion:
-  UriManager.uri * UriManager.uri * UriManager.uri -> unit
+  coerc_carr * coerc_carr * UriManager.uri -> unit
 
 val remove_coercion:
-  (UriManager.uri * UriManager.uri * UriManager.uri -> bool) -> unit
+  (coerc_carr * coerc_carr * UriManager.uri -> bool) -> unit
 
 val find_coercion:
-  (UriManager.uri * UriManager.uri -> bool) -> UriManager.uri list 
+  (coerc_carr * coerc_carr -> bool) -> UriManager.uri list