From 68df3763b02a1c274bd4394afde6ff67b6d8e539 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) --- helm/software/components/library/coercDb.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml index e0dc18d05..fae096229 100644 --- a/helm/software/components/library/coercDb.ml +++ b/helm/software/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