]> matita.cs.unibo.it Git - helm.git/commitdiff
Critical bug finally found after a long chasing!!!
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sun, 5 Nov 2006 16:14:41 +0000 (16:14 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sun, 5 Nov 2006 16:14:41 +0000 (16:14 +0000)
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

index ac57aa40a82b3f4fde03e07e588646ab10f40871..ed3d58c724c66cd71d8b3a5bc0b549aa9c75dbba 100644 (file)
@@ -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
 ;;