From b9531998071f8b6fafd2e32fea28051d35002cb6 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 30 Aug 2007 16:46:19 +0000
Subject: [PATCH] reverted assertion, since it may happen to look for a
 coercion to funclass even outside fix_arity (in cicRefine/eat_prods)

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

diff --git a/components/library/coercDb.ml b/components/library/coercDb.ml
index e0dc18d05..fae096229 100644
--- a/components/library/coercDb.ml
+++ b/components/library/coercDb.ml
@@ -41,7 +41,10 @@ let coerc_carr_of_term t =
  try
   match t with
    | Cic.Sort s -> Sort s
-   | Cic.Prod _ -> assert false
+   | Cic.Prod _ -> Fun 0 
+     (* BUG: this should be the real arity. The computation
+      requires menv, context etc.., but since carrs are compared discharging Fun
+      arity... it works *)
    | Cic.Appl (t::_)
    | t -> Uri (CicUtil.uri_of_term t)
  with Invalid_argument _ ->
-- 
2.39.2