X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcoercDb.ml;h=aec6dd5795bb9051adf78ce7336cc5f34cef6193;hb=7a39300df548240641269857e40d5476ff88db16;hp=2e93efa0eb8e09c43bc47b7946e83069491ac14c;hpb=5d010a40c726d9a7eceeb35e70e41a158eb63c70;p=helm.git

diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml
index 2e93efa0e..aec6dd579 100644
--- a/helm/software/components/library/coercDb.ml
+++ b/helm/software/components/library/coercDb.ml
@@ -66,9 +66,20 @@ let rec name_of_carr = function
   | Fun i -> "FunClass_" ^ string_of_int i   
 ;;
 
-let eq_carr src tgt =
+let eq_carr ?(exact=false) src tgt =
   match src, tgt with
-  | Uri src, Uri tgt -> UriManager.eq src tgt
+  | Uri src, Uri tgt -> 
+      let coarse_eq = UriManager.eq src tgt in
+      let src_noxpointer = UriManager.strip_xpointer src in
+      if exact && coarse_eq && UriManager.uri_is_ind src_noxpointer then
+        match 
+          fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph src_noxpointer)
+        with
+        | Cic.InductiveDefinition (_,[],m,_) when m = 0 -> true
+        | Cic.Constant _ -> true
+        | _ -> false
+      else
+        coarse_eq
   | Sort (Cic.Type _), Sort (Cic.Type _) -> true
   | Sort src, Sort tgt when src = tgt -> true
   | Term t1, Term t2 ->