fixed undo support for coercions inside records

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

diff --git a/helm/ocaml/library/coercDb.mli b/helm/ocaml/library/coercDb.mli
index 970d2b98a803b5298055f3af7abc771ed575f0ad..9e8bf5e9c03066cf219921ac66baaed7a96918d5 100644 (file)
--- a/helm/ocaml/library/coercDb.mli
+++ b/helm/ocaml/library/coercDb.mli
@@ -24,7 +24,11 @@
  *)
 
 
- (** THIS MODULE SHOULD BE USED ONLY BY CoercGraph **)
+ (** THIS MODULE SHOULD BE USED ONLY BY CoercGraph/CicCoercion/librarySync
+  * 
+  *   and may be merged with CicCoercion...
+  *  
+  * **)
 
 
   (** XXX WARNING: non-reentrant *)
@@ -51,4 +55,4 @@ val find_coercion:
 val is_a_coercion: UriManager.uri -> bool
 val get_carr: UriManager.uri -> coerc_carr * coerc_carr
 
-
+val term_of_carr: coerc_carr -> Cic.term