X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Flibrary%2FcoercGraph.mli;h=bd562414ee0e457c16240738ed3208c5dd03a521;hb=6c15f0679a74ff8e8f51e01590bc5eb8e0567fc5;hp=fcbed3497313fd840b81d36000d5e3eef7d3dd6a;hpb=727ef55d2a6202a989c274f6caa1b0e1b7307880;p=helm.git

diff --git a/helm/ocaml/library/coercGraph.mli b/helm/ocaml/library/coercGraph.mli
index fcbed3497..bd562414e 100644
--- a/helm/ocaml/library/coercGraph.mli
+++ b/helm/ocaml/library/coercGraph.mli
@@ -32,8 +32,10 @@ type coercion_search_result =
 val look_for_coercion :
   Cic.term -> Cic.term -> coercion_search_result
 
-(* also adds them to the Db *)
-val close_coercion_graph:
-  CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
-    (UriManager.uri * Cic.obj * CicUniv.universe_graph) list
+(* it returns the list of composite coercions and their auxiliary lemmas  *)
+(* composite coercions are always declared as such; they are added to the *)
+(* library only on demand (i.e. not when processing a .moo)               *)
+val add_coercion:
+ basedir:string -> add_composites:bool -> UriManager.uri -> UriManager.uri list
 
+val remove_coercion: UriManager.uri -> unit