From 9ff32d2a3efcf850ea52fe0223a5152f8777aee5 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 14 Apr 2006 10:11:32 +0000
Subject: [PATCH] 	added minimal euristic for generic terms carrier
 comparison

---
 helm/software/components/library/coercDb.ml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml
index c5356b3e1..8b7982ea0 100644
--- a/helm/software/components/library/coercDb.ml
+++ b/helm/software/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