X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fcompose.ml;h=cd355dc2785049d44dd78630401ea1884a052087;hb=1f6aab137983a515b3ba4bb1d1efe0c9e22e889e;hp=137e919b09fd98e6c5d6da3f5f155cd79b7850c6;hpb=5d1cece5f42866b34566a0f616aa3b46a77359a3;p=helm.git

diff --git a/helm/software/components/tactics/compose.ml b/helm/software/components/tactics/compose.ml
index 137e919b0..cd355dc27 100644
--- a/helm/software/components/tactics/compose.ml
+++ b/helm/software/components/tactics/compose.ml
@@ -79,7 +79,7 @@ let compose_core t2 t1 (proof, goal) =
       try
         let t, menv1, _ =
           CloseCoercionGraph.generate_composite t2 t1 context menv
-            CicUniv.oblivion_ugraph arity false
+            CicUniv.oblivion_ugraph arity
         in
         assert (List.length menv1 = List.length menv);
         generate tl menv (t::acc)