X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcoercDb.mli;h=d8a8b0574de506f222da61acfb073f9074723896;hb=abd2098b6c4a40b36bb4b950c607eb4b4a7852bc;hp=9e8bf5e9c03066cf219921ac66baaed7a96918d5;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/library/coercDb.mli b/helm/software/components/library/coercDb.mli
index 9e8bf5e9c..d8a8b0574 100644
--- a/helm/software/components/library/coercDb.mli
+++ b/helm/software/components/library/coercDb.mli
@@ -32,16 +32,23 @@
 
 
   (** XXX WARNING: non-reentrant *)
-type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term
+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 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
+    (coerc_carr * coerc_carr * UriManager.uri list) list
 
 val add_coercion:
   coerc_carr * coerc_carr * UriManager.uri -> unit
@@ -56,3 +63,4 @@ val is_a_coercion: UriManager.uri -> bool
 val get_carr: UriManager.uri -> coerc_carr * coerc_carr
 
 val term_of_carr: coerc_carr -> Cic.term
+