-(* XXX saturate takes no subst!!!! *)
-let look_for_coercion (db_src,db_tgt) metasenv _subst context infty expty =
- let set_src = DB.retrieve_unifiables db_src infty in
- let set_tgt = DB.retrieve_unifiables db_tgt expty in
- let candidates = CoercionSet.inter set_src set_tgt in
- prerr_endline "aaaaaaaaaaaaa";
- List.map
- (fun (t,arity,arg) ->
- let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t in
- let ty, metasenv, args =
- NCicMetaSubst.saturate ~delta:max_int metasenv context ty arity
- in
- prerr_endline (
- NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^
- NCicPp.ppterm ~metasenv ~subst:_subst ~context
- (NCicUntrusted.mk_appl t args) ^ " --- " ^
- string_of_int (List.length args) ^ " == " ^ string_of_int arg);
- metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
- (CoercionSet.elements candidates)
+let empty_db = (DB.empty,DB.empty) ;;
+
+
+let look_for_coercion (db_src,db_tgt) metasenv subst context infty expty =
+ match infty, expty with
+ | (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)),
+ (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> []
+ | _ ->
+(*
+ prerr_endline ("LOOK FOR COERCIONS: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context infty ^ " |===> " ^
+ NCicPp.ppterm ~metasenv ~subst ~context expty);
+*)
+ let set_src = DB.retrieve_unifiables db_src infty in
+ let set_tgt = DB.retrieve_unifiables db_tgt expty in
+ let candidates = CoercionSet.inter set_src set_tgt in
+(*
+ prerr_endline ("CANDIDATES: " ^
+ String.concat "," (List.map (fun (t,_,_) ->
+ NCicPp.ppterm ~metasenv ~subst ~context t)
+ (CoercionSet.elements candidates)));
+*)
+ List.map
+ (fun (t,arity,arg) ->
+ let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t in
+ let ty, metasenv, args =
+ NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity
+ in
+ (* prerr_endline (
+ NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^
+ NCicPp.ppterm ~metasenv ~subst ~context
+ (NCicUntrusted.mk_appl t args) ^ " --- " ^
+ string_of_int (List.length args) ^ " == " ^ string_of_int arg); *)
+ metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
+ (CoercionSet.elements candidates)