X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicCoercion.ml;h=e62d4eed324d7489226e77fda3e7d86f27e7f9ec;hb=8de1a75899a83dd31e856804bd448c1bd87d9ab3;hp=a4b10296f2f5f960d7074285abebcc34bccb3cbd;hpb=84e770b58ae08a345087de816aba29bc2fc727ba;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index a4b10296f..e62d4eed3 100644
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -37,11 +37,12 @@ let index_coercion (db_src,db_tgt) c src tgt arity arg =
   db_src, db_tgt
 ;;
 
-let db () =
+let index_old_db odb db =
   List.fold_left 
     (fun db (_,tgt,clist) -> 
        List.fold_left 
          (fun db (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,9 +67,12 @@ let db () =
                     NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t);
                   assert false
             in
-            index_coercion db c src tgt arity arg)
+            index_coercion db c src tgt arity arg
+           with 
+           | NCicEnvironment.BadDependency _ 
+           | NCicTypeChecker.TypeCheckerFailure _ -> db)
          db clist)
-    (DB.empty,DB.empty) (CoercDb.to_list ())
+    db (CoercDb.to_list odb)
 ;;
 
 let empty_db = (DB.empty,DB.empty) ;;