compose tactic restore and added nocomposites keyword

[helm.git] / components / library / coercDb.ml

diff --git a/components/library/coercDb.ml b/components/library/coercDb.ml
index 14ddf7c8631b5054aca10a8accc0268e9c12b05f..0ca40eb1c2860cef5da6d5def71040cfb7422234 100644 (file)
--- 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 ->