From 32ef836432653401022519318957408bcfc64e27 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 2 Jun 2007 09:38:35 +0000
Subject: [PATCH] wrong assertion was inserted, now just a warning to know when
 it happens

---
 helm/software/components/tactics/closeCoercionGraph.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml
index 1f4c1d12b..4f1d1b182 100644
--- a/helm/software/components/tactics/closeCoercionGraph.ml
+++ b/helm/software/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
-- 
2.39.2