huge commit regarding the grafite_status:

[helm.git] / helm / software / components / ng_refiner / nCicCoercion.ml

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index a4b10296f2f5f960d7074285abebcc34bccb3cbd..e62d4eed324d7489226e77fda3e7d86f27e7f9ec 100644 (file)
--- 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) ;;