COERCIONS: tentative addition of an equivalence relation over coercion source

[helm.git] / helm / software / components / library / coercDb.mli

diff --git a/helm/software/components/library/coercDb.mli b/helm/software/components/library/coercDb.mli
index 95dd96c0b18a2fd9a3849a8b707b74b1e1a7e38a..e6d7e46b30042778b6b3889970c56dac329741bd 100644 (file)
--- a/helm/software/components/library/coercDb.mli
+++ b/helm/software/components/library/coercDb.mli
@@ -36,12 +36,15 @@ 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 -> 
@@ -57,6 +60,8 @@ val find_coercion:
   (coerc_carr * coerc_carr -> bool) -> UriManager.uri 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