Critical bug finally found after a long chasing!!!

When looking for a coercion over a non meta closed term, often the case was
not detected and a Failure was raised instead of Uncertain.

diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml
index ac57aa40a82b3f4fde03e07e588646ab10f40871..ed3d58c724c66cd71d8b3a5bc0b549aa9c75dbba 100644 (file)
--- a/helm/software/components/library/coercDb.ml
+++ b/helm/software/components/library/coercDb.ml
@@ -82,6 +82,8 @@ let eq_carr src tgt =
       else raise EqCarrOnNonMetaClosed
   | Fun _,Fun _ -> true (* only one Funclass? *)
 (*   | Fun i,Fun j when i=j -> true *)
+  | Term t, _
+  | _, Term t when not (CicUtil.is_meta_closed t) -> raise EqCarrOnNonMetaClosed
   | _, _ -> false
 ;;