X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcoercDb.ml;h=ed3d58c724c66cd71d8b3a5bc0b549aa9c75dbba;hb=a45b20401c52a767eb8fef71a72be6dc5db8a02a;hp=ac57aa40a82b3f4fde03e07e588646ab10f40871;hpb=7cf5f62b28abd2e367014e164a2635ae41bcf519;p=helm.git

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
 ;;