Fixed a call to auto, and commented the remaining part.

[helm.git] / helm / software / components / library / coercDb.ml

diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml
index 9a1fdb0ea85de8434cf529ccfa183151960fb455..ed3d58c724c66cd71d8b3a5bc0b549aa9c75dbba 100644 (file)
--- a/helm/software/components/library/coercDb.ml
+++ b/helm/software/components/library/coercDb.ml
@@ -40,7 +40,8 @@ let db = ref []
 let coerc_carr_of_term t =
  try
   match t with
-     Cic.Sort s -> Sort s
+   | Cic.Sort s -> Sort s
+   | Cic.Prod _ -> Fun 0
    | Cic.Appl (t::_)
    | t -> Uri (CicUtil.uri_of_term t)
  with Invalid_argument _ ->
@@ -81,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
 ;;