]> matita.cs.unibo.it Git - helm.git/blobdiff - components/library/coercDb.mli
Coercions are now generalized to the general form
[helm.git] / components / library / coercDb.mli
index e6d7e46b30042778b6b3889970c56dac329741bd..e1afd61aa0eb2cd3272da19819b9eefbc2bc9c24 100644 (file)
@@ -48,16 +48,16 @@ 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