carr_of_term now returns Fun if a Prod is encountered

diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml
index 9a1fdb0ea85de8434cf529ccfa183151960fb455..ac57aa40a82b3f4fde03e07e588646ab10f40871 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 _ ->