1. The last commit that fixed unification of compound coercions with

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

diff --git a/helm/ocaml/library/librarySync.mli b/helm/ocaml/library/librarySync.mli
index 43ac34da32865e6ed587efb7c48c22dbc8b6a622..d063b3282734b354c6b822467329e7a558149f14 100644 (file)
--- a/helm/ocaml/library/librarySync.mli
+++ b/helm/ocaml/library/librarySync.mli
@@ -25,6 +25,8 @@
 
 exception AlreadyDefined of UriManager.uri
 
+val merge_coercions: Cic.term -> Cic.term
+
 (* adds an object to the library together with all auxiliary lemmas on it *)
 (* (e.g. elimination principles, projections, etc.)                       *)
 (* it returns the list of the uris of the auxiliary lemmas generated      *)