COERCIONS: tentative addition of an equivalence relation over coercion source

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

diff --git a/components/library/coercDb.ml b/components/library/coercDb.ml
index 2e93efa0eb8e09c43bc47b7946e83069491ac14c..aec6dd5795bb9051adf78ce7336cc5f34cef6193 100644 (file)
--- 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 ->