+let check_for_duplicates metas msg =
+ let rec aux = function
+ | [] -> true
+ | (m,_,_)::tl ->
+ not (List.exists (fun (i, _, _) -> i = m) tl) && aux tl in
+ let b = aux metas in
+ if not b then
+ begin
+ prerr_endline ("DUPLICATI ---- " ^ msg);
+ prerr_endline (CicMetaSubst.ppmetasenv [] metas);
+ assert false
+ end
+ else b
+;;
+
+let check_metasenv msg menv =
+ List.iter
+ (fun (i,ctx,ty) ->
+ try ignore(CicTypeChecker.type_of_aux' menv ctx ty
+ CicUniv.empty_ugraph)
+ with
+ | CicUtil.Meta_not_found _ ->
+ prerr_endline (msg ^ CicMetaSubst.ppmetasenv [] menv);
+ assert false
+ | _ -> ()
+ ) menv
+;;
+