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

[helm.git] / helm / software / components / tactics / compose.ml

diff --git a/helm/software/components/tactics/compose.ml b/helm/software/components/tactics/compose.ml
index 137e919b09fd98e6c5d6da3f5f155cd79b7850c6..cd355dc2785049d44dd78630401ea1884a052087 100644 (file)
--- 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)