X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FcoercDb.ml;h=aec6dd5795bb9051adf78ce7336cc5f34cef6193;hb=975ad45cc779a6bee3d450a006347cc23ca3977e;hp=2e93efa0eb8e09c43bc47b7946e83069491ac14c;hpb=6bb370c6e1a036e82315765d6dceb1939c30ed23;p=helm.git

diff --git a/components/library/coercDb.ml b/components/library/coercDb.ml
index 2e93efa0e..aec6dd579 100644
--- a/components/library/coercDb.ml
+++ b/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 ->