| x::tl -> x :: replace_in_metasenv i f tl
;;
+let rec replace_in_subst i f = function
+ | [] -> assert false
+ | (j,e)::tl when j=i -> (i,f e) :: tl
+ | x::tl -> x :: replace_in_subst i f tl
+;;
+
let set_kind newkind attrs =
newkind :: List.filter (fun x -> not (is_kind x)) attrs
;;