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: make_still_working~6753
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7cf5f62b28abd2e367014e164a2635ae41bcf519;p=helm.git

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 9a1fdb0ea..ac57aa40a 100644
--- 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 _ ->