From 9dc727beb31286d228834cb6bce7afa242363477 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 5 Nov 2006 16:14:41 +0000 Subject: [PATCH] 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. --- components/library/coercDb.ml | 2 ++ 1 file changed, 2 insertions(+) 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 ;; -- 2.39.2