From 6ea07c7b5d378a25eb6c9b3134aec642b86cd79c 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. --- helm/software/components/library/coercDb.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml index ac57aa40a..ed3d58c72 100644 --- 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 ;; -- 2.39.2