X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FcloseCoercionGraph.mli;h=baf926ff156e37d1d685a7a38c54e6127eeaed03;hb=1f6aab137983a515b3ba4bb1d1efe0c9e22e889e;hp=1acea0eebda80bf37a24585ea78933b47dcb6a9f;hpb=4f7cc852e331ab1cfa7f6085171873a77b87e4ce;p=helm.git

diff --git a/helm/software/components/tactics/closeCoercionGraph.mli b/helm/software/components/tactics/closeCoercionGraph.mli
index 1acea0eeb..baf926ff1 100644
--- a/helm/software/components/tactics/closeCoercionGraph.mli
+++ b/helm/software/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