X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcoercDb.ml;h=80222ad341f9d0ae8be79861a64735e03c46cbdc;hb=ca41435a6021292ccba239aa173651c0be705b45;hp=14ddf7c8631b5054aca10a8accc0268e9c12b05f;hpb=4941c45d05f0708774f614a89c1dbaf3ec171c52;p=helm.git

diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml
index 14ddf7c86..80222ad34 100644
--- a/helm/software/components/library/coercDb.ml
+++ b/helm/software/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 ->
@@ -194,3 +190,7 @@ let add_coercion (src,tgt,u,saturations) =
         db := (src,tgt,(u,1,saturations)::l)::tl @ rest
       
 ;;
+
+type coerc_db = (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list 
+let dump () = !db 
+let restore coerc_db = db := coerc_db