Coercions are now generalized to the general form

[helm.git] / components / tactics / closeCoercionGraph.mli

diff --git a/components/tactics/closeCoercionGraph.mli b/components/tactics/closeCoercionGraph.mli
index 8750ce0f7888f2bb359b5624aef88404d58bb376..1acea0eebda80bf37a24585ea78933b47dcb6a9f 100644 (file)
--- a/components/tactics/closeCoercionGraph.mli
+++ b/components/tactics/closeCoercionGraph.mli
@@ -26,9 +26,10 @@
 (* This module implements the Coercions transitive closure *)
 
 val close_coercion_graph:
-  CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
+  CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
   string (* baseuri *) ->
-    (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list
+    (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj)
+      list
 
 exception UnableToCompose