1. composition of coercions with saturations > 0 is now implemented

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

diff --git a/components/tactics/closeCoercionGraph.mli b/components/tactics/closeCoercionGraph.mli
index 1acea0eebda80bf37a24585ea78933b47dcb6a9f..baf926ff156e37d1d685a7a38c54e6127eeaed03 100644 (file)
--- a/components/tactics/closeCoercionGraph.mli
+++ b/components/tactics/closeCoercionGraph.mli
@@ -36,5 +36,4 @@ exception UnableToCompose
 val generate_composite:
   Cic.term -> Cic.term -> Cic.context -> 
   Cic.metasenv -> CicUniv.universe_graph -> int (* arity *) -> 
-    bool (* last lambda goes with innermost arg *) ->
     Cic.term * Cic.metasenv * CicUniv.universe_graph