(* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *)
let debug s = prerr_endline (Lazy.force s);;
-let debug _ = ();;
+(* let debug _ = ();; *)
module COT : Set.OrderedType
with type t = string * NCic.term * int * int * NCic.term *
let look_for_coercion status metasenv subst context infty expty =
let db_src,db_tgt = status#coerc_db in
- match infty, expty with
+ match
+ NCicUntrusted.apply_subst subst context infty,
+ NCicUntrusted.apply_subst subst context expty
+ with
| (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)),
(NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> []
- | _ ->
+ | infty, expty ->
debug (lazy ("LOOK FOR COERCIONS: " ^
NCicPp.ppterm ~metasenv ~subst ~context infty ^ " |===> " ^
CoercionSet.union (DB.retrieve_unifiables db_tgt expty) set)
CoercionSet.empty tgt_class
in
+
+ debug (lazy ("CANDIDATES SRC: " ^
+ String.concat "," (List.map (fun (name,t,_,_,_,_) ->
+ name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t)
+ (CoercionSet.elements set_src))));
+ debug (lazy ("CANDIDATES TGT: " ^
+ String.concat "," (List.map (fun (name,t,_,_,_,_) ->
+ name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t)
+ (CoercionSet.elements set_tgt))));
+
let candidates = CoercionSet.inter set_src set_tgt in
debug (lazy ("CANDIDATES: " ^