From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 5 Nov 2006 16:14:41 +0000 (+0000)
Subject: Critical bug finally found after a long chasing!!!
X-Git-Tag: 0.4.95@7852~821
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9dc727beb31286d228834cb6bce7afa242363477;p=helm.git

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/components/library/coercDb.ml b/components/library/coercDb.ml
index ac57aa40a..ed3d58c72 100644
--- a/components/library/coercDb.ml
+++ b/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
 ;;