X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicCoercion.ml;h=73da9579f078a8e8b5ec45914ff9fbe2f6255ed9;hb=3ace6e853d2cb8ce8c98b7d8c07a4f6c6b61ba84;hp=04fddee83fdee339546a4bf42484bdf3e23d8f73;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/ng_refiner/nCicCoercion.ml b/matita/components/ng_refiner/nCicCoercion.ml
index 04fddee83..73da9579f 100644
--- a/matita/components/ng_refiner/nCicCoercion.ml
+++ b/matita/components/ng_refiner/nCicCoercion.ml
@@ -64,44 +64,6 @@ let index_coercion status name c src tgt arity arg =
   status#set_coerc_db (db_src, db_tgt)
 ;;
 
-let index_old_db odb (status : #status) =
-  List.fold_left 
-    (fun status (_,tgt,clist) -> 
-       List.fold_left 
-         (fun status (uri,_,arg) ->
-           try
-            let c=fst (!convert_term uri (CicUtil.term_of_uri uri)) in
-            let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in
-            let src, tgt = 
-              let cty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] c in
-              let scty, metasenv,_ = 
-                NCicMetaSubst.saturate ~delta:max_int [] [] [] cty (arity+1) 
-              in
-              match scty with
-              | NCic.Prod (_, src, tgt) -> 
-                 let tgt =
-                   NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt
-                 in
-(*
-            debug (lazy (Printf.sprintf "indicizzo %s (%d)) : %s ===> %s" 
-              (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] scty) (arity+1)
-              (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] src)
-              (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] tgt));
-*)
-                src, tgt
-              | t -> 
-                  debug (lazy (
-                    NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t));
-                  assert false
-            in
-            index_coercion status "foo" c src tgt arity arg
-           with 
-           | NCicEnvironment.BadDependency _ 
-           | NCicTypeChecker.TypeCheckerFailure _ -> status)
-         status clist)
-    status (CoercDb.to_list odb)
-;;
-
 let look_for_coercion status metasenv subst context infty expty =
  let db_src,db_tgt = status#coerc_db in
   match