From d9a1441c59bd7f20ef2c47d40bd29d4253f54876 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 14 Apr 2006 10:11:32 +0000 Subject: [PATCH] added minimal euristic for generic terms carrier comparison --- components/library/coercDb.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/components/library/coercDb.ml b/components/library/coercDb.ml index c5356b3e1..8b7982ea0 100644 --- a/components/library/coercDb.ml +++ b/components/library/coercDb.ml @@ -59,12 +59,14 @@ let eq_carr src tgt = | Sort (Cic.Type _), Sort (Cic.Type _) -> true | Sort src, Sort tgt when src = tgt -> true | Term t1, Term t2 -> - if CicUtil.is_meta_closed t1 && CicUtil.is_meta_closed t2 then - raise - (EqCarrNotImplemented + if t1 = t2 then true + else + if CicUtil.is_meta_closed t1 && CicUtil.is_meta_closed t2 then + raise + (EqCarrNotImplemented (lazy ("Unsupported carr for coercions: " ^ - CicPp.ppterm t1 ^ " or " ^ CicPp.ppterm t2))) - else raise EqCarrOnNonMetaClosed + CicPp.ppterm t1 ^ " or " ^ CicPp.ppterm t2))) + else raise EqCarrOnNonMetaClosed | _, _ -> false let to_list () = -- 2.39.2