- with exn -> prerr_endline ("PIPPO" ^ Printexc.to_string exn); empty_db
-
-(* List.fold_left
- (fun db (_,tgt,clist) ->
- List.fold_left
- (fun db (uri,_,arg) ->
- 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 =
- 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
-(*
- prerr_endline (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 ->
- prerr_endline (
- 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 ())
- *)