X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcoercDb.mli;h=3071aecc4eb724064849f21da4fc8bcc8314d099;hb=ed5c4e15429c37bef0f59dfd7160f6883586ed0f;hp=92d4b7f2484e231e1547a62899fe094ece785c79;hpb=6fb856f244035ba071d60a158fa800104f50072a;p=helm.git

diff --git a/helm/software/components/library/coercDb.mli b/helm/software/components/library/coercDb.mli
index 92d4b7f24..3071aecc4 100644
--- a/helm/software/components/library/coercDb.mli
+++ b/helm/software/components/library/coercDb.mli
@@ -36,28 +36,36 @@ type coerc_carr =
   | Uri of UriManager.uri (* const, mutind, mutconstr *)
   | Sort of Cic.sort (* Prop, Set, Type *) 
   | Term of Cic.term (* nothing supported *)
+  | Fun of int
+;;
   
 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
+
+type coerc_db
+val dump: unit -> coerc_db
+val restore: coerc_db -> unit
 
 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
+val is_a_coercion_to_funclass: Cic.term -> int option
 val get_carr: UriManager.uri -> coerc_carr * coerc_carr
 
 val term_of_carr: coerc_carr -> Cic.term