X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FcoercDb.mli;h=e1afd61aa0eb2cd3272da19819b9eefbc2bc9c24;hb=65662e7d8de61a338b636f208d04e85eb59e6b8e;hp=5f455c2af97dd6146bddeebd64c0f281ce0b6334;hpb=6bb370c6e1a036e82315765d6dceb1939c30ed23;p=helm.git

diff --git a/components/library/coercDb.mli b/components/library/coercDb.mli
index 5f455c2af..e1afd61aa 100644
--- a/components/library/coercDb.mli
+++ b/components/library/coercDb.mli
@@ -41,23 +41,23 @@ type coerc_carr =
   
 exception EqCarrNotImplemented of string Lazy.t
 exception EqCarrOnNonMetaClosed
-val eq_carr: coerc_carr -> coerc_carr -> bool
+val eq_carr: ?exact:bool -> coerc_carr -> coerc_carr -> bool
 val coerc_carr_of_term: Cic.term -> coerc_carr
 val name_of_carr: coerc_carr -> string
 val uri_of_carr: coerc_carr -> UriManager.uri option
 
 val to_list:
   unit -> 
-    (coerc_carr * coerc_carr * UriManager.uri list) list
+    (coerc_carr * coerc_carr * (UriManager.uri * int) list) list
 
 val add_coercion:
-  coerc_carr * coerc_carr * UriManager.uri -> unit
+  coerc_carr * coerc_carr * UriManager.uri * int -> unit
 
 val remove_coercion:
-  (coerc_carr * coerc_carr * UriManager.uri -> bool) -> unit
+  (coerc_carr * coerc_carr * UriManager.uri * int -> bool) -> unit
 
 val find_coercion: 
-  (coerc_carr * coerc_carr -> bool) -> UriManager.uri list 
+  (coerc_carr * coerc_carr -> bool) -> (UriManager.uri * int) list 
     
 val is_a_coercion: UriManager.uri -> bool
 val is_a_coercion': Cic.term -> bool