X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FcoercDb.ml;h=0ca40eb1c2860cef5da6d5def71040cfb7422234;hb=b0a6c05decc9f0e731f70cfc5ae5350ae4046b79;hp=14ddf7c8631b5054aca10a8accc0268e9c12b05f;hpb=864b6ef1956a312e5401a8705bcf7cf0cccf4e9f;p=helm.git

diff --git a/components/library/coercDb.ml b/components/library/coercDb.ml
index 14ddf7c86..0ca40eb1c 100644
--- a/components/library/coercDb.ml
+++ b/components/library/coercDb.ml
@@ -73,16 +73,12 @@ let eq_carr ?(exact=false) src tgt =
   match src, tgt with
   | 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
+      let t = CicUtil.term_of_uri src in
+      let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph in
+      (match ty, exact with
+      | Cic.Prod _, true -> false
+      | Cic.Prod _, false -> coarse_eq
+      | _ -> coarse_eq) 
   | Sort (Cic.Type _), Sort (Cic.Type _) -> true
   | Sort src, Sort tgt when src = tgt -> true
   | Term t1, Term t2 ->