]> matita.cs.unibo.it Git - helm.git/blobdiff - components/library/coercDb.mli
...
[helm.git] / components / library / coercDb.mli
index 5f455c2af97dd6146bddeebd64c0f281ce0b6334..e1afd61aa0eb2cd3272da19819b9eefbc2bc9c24 100644 (file)
@@ -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