From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 30 Aug 2007 13:13:56 +0000 (+0000)
Subject: coercions from funclass are not supported
X-Git-Tag: 0.4.95@7852~241
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dfdcf89229ed6c5c21958205ed2fff9c29d11803;p=helm.git

coercions from funclass are not supported
---

diff --git a/components/library/coercDb.ml b/components/library/coercDb.ml
index aec6dd579..1f3874912 100644
--- a/components/library/coercDb.ml
+++ b/components/library/coercDb.ml
@@ -41,7 +41,7 @@ let coerc_carr_of_term t =
  try
   match t with
    | Cic.Sort s -> Sort s
-   | Cic.Prod _ -> Fun 0
+   | Cic.Prod _ -> assert false
    | Cic.Appl (t::_)
    | t -> Uri (CicUtil.uri_of_term t)
  with Invalid_argument _ ->