X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FcloseCoercionGraph.ml;h=4f1d1b182159eb334710bff22b2caa8a57d1e139;hb=614e3c3fb219e404e60810bfc04072351803b8e8;hp=1f4c1d12b2182055ddf994bcfb9110475ac25e4e;hpb=51618b89bbe3cd86fc079d593c8a169dc304b189;p=helm.git

diff --git a/components/tactics/closeCoercionGraph.ml b/components/tactics/closeCoercionGraph.ml
index 1f4c1d12b..4f1d1b182 100644
--- a/components/tactics/closeCoercionGraph.ml
+++ b/components/tactics/closeCoercionGraph.ml
@@ -341,7 +341,9 @@ let close_coercion_graph src tgt uri baseuri =
                             (CoercDb.term_of_carr (CoercDb.Uri coer)) 
                             [] [] univ arity true
                         in
-                        assert (menv = []);
+                        if (menv = []) then
+                          prerr_endline 
+                            "MENV non empty after composing coercions";
                         build_obj t univ arity
                     | _ -> assert false 
                   ) (first_step, CicUniv.empty_ugraph) tl