+let coerced_arg l =
+ match l with
+ | [] | [_] -> assert false
+ | c::_ when not (CoercDb.is_a_coercion' c) -> assert false
+ | c::tl ->
+ 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
+;;
+
+(************************* meet calculation stuff ********************)
+let eq_uri_opt u1 u2 =
+ match u1,u2 with
+ | Some (u1,_), Some (u2,_) -> UriManager.eq u1 u2
+ | None,Some _ | Some _, None -> false
+ | None, None -> true
+;;
+
+let eq_carr_uri (c1,u1) (c2,u2) = CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2;;
+
+let eq_carr_uri_uri (c1,u1,u11) (c2,u2,u22) =
+ CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2 && eq_uri_opt u11 u22
+;;
+
+let uniq = HExtlib.list_uniq ~eq:eq_carr_uri;;
+
+let uniq2 = HExtlib.list_uniq ~eq:eq_carr_uri_uri;;