From b9531998071f8b6fafd2e32fea28051d35002cb6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi 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