+
+(* CSC: very inefficient implementation!
+ Enrico, can we use a discrimination tree here? *)
+let match_coercion status ~metasenv ~subst ~context t =
+ let db =
+ DB.fold (fst (status#coerc_db)) (fun _ v l -> (CoercionSet.elements v)@l) []
+ in
+ try
+ Some
+ (List.find
+ (fun (p,_,_) ->
+ try
+ let t =
+ match p,t with
+ NCic.Appl lp, NCic.Appl lt ->
+ (match fst (HExtlib.split_nth (List.length lp) lt) with
+ [t] -> t
+ | l -> NCic.Appl l)
+ | _,NCic.Appl (he::_) -> he
+ | _,_ -> t
+ in
+ NCicReduction.alpha_eq metasenv subst context p t
+ with
+ Failure _ -> false (* raised by split_nth *)
+ ) db)
+ with
+ Not_found -> None
+;;