From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 12 Oct 2006 16:10:53 +0000 (+0000)
Subject: carr_of_term now returns Fun if a Prod is encountered
X-Git-Tag: 0.4.95@7852~894
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3afed401e6dd094eb0e6278138dc3ff012b7d63b;p=helm.git

carr_of_term now returns Fun if a Prod is encountered
---

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