From 3afed401e6dd094eb0e6278138dc3ff012b7d63b Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 12 Oct 2006 16:10:53 +0000
Subject: [PATCH] carr_of_term now returns Fun if a Prod is encountered

---
 components/library/coercDb.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/components/library/coercDb.ml b/components/library/coercDb.ml
index 9a1fdb0ea..ac57aa40a 100644
--- a/components/library/coercDb.ml
+++ b/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 _ ->
-- 
2.39.2