X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicCoercion.ml;h=29f28ba5c3a4608269b5245b500ee7fd8f3b268f;hb=8bc5bc0e8375a85736f6a5df317d129d5efa8de4;hp=f2467605f085731d456816feb325ca2e30e4b56a;hpb=10634c47be2ece4c088a1a1c1be5163952bf1c42;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index f2467605f..29f28ba5c 100644
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -24,7 +24,17 @@ module DB =
 
 type db = DB.t * DB.t
 
-let index_coercion (db_src,db_tgt) c src tgt arity arg =
+let empty_db = DB.empty,DB.empty
+
+class status =
+ object
+  val db = empty_db
+  method coerc_db = db
+  method set_coerc_db v = {< db = v >}
+ end
+
+let index_coercion status c src tgt arity arg =
+  let db_src,db_tgt = status#coerc_db in
   let data = (c,arity,arg) in
 (*
   prerr_endline ("INDEX:" ^ 
@@ -34,14 +44,15 @@ let index_coercion (db_src,db_tgt) c src tgt arity arg =
 *)
   let db_src = DB.index db_src src data in
   let db_tgt = DB.index db_tgt tgt data in
-  db_src, db_tgt
+  status#set_coerc_db (db_src, db_tgt)
 ;;
 
-let db () =
+let index_old_db odb (status : #status) =
   List.fold_left 
-    (fun db (_,tgt,clist) -> 
+    (fun status (_,tgt,clist) -> 
        List.fold_left 
-         (fun db (uri,_,arg) ->
+         (fun status (uri,_,arg) ->
+           try
             let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in
             let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in
             let src, tgt = 
@@ -66,12 +77,16 @@ let db () =
                     NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t);
                   assert false
             in
-            index_coercion db c src tgt arity arg)
-         db clist)
-    (DB.empty,DB.empty) (CoercDb.to_list ())
+            index_coercion status c src tgt arity arg
+           with 
+           | NCicEnvironment.BadDependency _ 
+           | NCicTypeChecker.TypeCheckerFailure _ -> status)
+         status clist)
+    status (CoercDb.to_list odb)
 ;;
 
-let look_for_coercion (db_src,db_tgt) metasenv subst context infty expty =
+let look_for_coercion status metasenv subst context infty expty =
+ let db_src,db_tgt = status#coerc_db in
   match infty, expty with
   | (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)), 
     (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> []