- let arity =
- match CoercDb.is_a_coercion_to_funclass c with None -> 0 | Some a -> a
- in
- (* decide a decent structure for coercion carriers so that all this stuff is
- * useless *)
- let pi =
- (* this calculation is not complete, since we have strange carriers *)
- let rec count_pi = function
- | Cic.Prod(_,_,t) -> 1+ (count_pi t)
- | _ -> 0
- in
- let uri = CicUtil.uri_of_term c in
- match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
- | Cic.Constant (_, _, ty, _, _) -> count_pi ty
- | _ -> assert false
- in
- try Some (List.nth tl (pi - arity)) with Invalid_argument _ -> None
+ match CoercDb.is_a_coercion c with
+ | None -> None
+ | Some (_,_,_,_,cpos) ->
+ if List.length tl > cpos then Some (List.nth tl cpos, cpos) else None