added support for "polymorphic" coercions

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

diff --git a/components/library/coercDb.mli b/components/library/coercDb.mli
index 9e8bf5e9c03066cf219921ac66baaed7a96918d5..1f5df89334352f3a299d5ee83ec8f044005c68a3 100644 (file)
--- a/components/library/coercDb.mli
+++ b/components/library/coercDb.mli
@@ -32,7 +32,11 @@
 
 
   (** 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 *)
+  
 exception EqCarrNotImplemented of string Lazy.t
 exception EqCarrOnNonMetaClosed
 val eq_carr: coerc_carr -> coerc_carr -> bool
@@ -56,3 +60,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
+