(* hide optional arg *)
let apply_subst s c t = apply_subst s c t;;
+
+type meta_kind = [ `IsSort | `IsType | `IsTerm ]
+
+let is_kind x = x = `IsSort || x = `IsType || x = `IsTerm ;;
+
+let kind_of_meta l =
+ try
+ (match List.find is_kind l with
+ | `IsSort | `IsType | `IsTerm as x -> x
+ | _ -> assert false)
+ with
+ Not_found -> assert false
+;;
+
+let rec replace_in_metasenv i f = function
+ | [] -> assert false
+ | (j,e)::tl when j=i -> (i,f e) :: tl
+ | 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
+;;
+
+let max_kind k1 k2 =
+ match k1, k2 with
+ | `IsSort, _ | _, `IsSort -> `IsSort
+ | `IsType, _ | _, `IsType -> `IsType
+ | _ -> `IsTerm
+;;
+