+let rec flexible_arg subst = function
+ | NCic.Meta (i,_) | NCic.Appl (NCic.Meta (i,_) :: _)->
+ (try
+ let _,_,t,_ = List.assoc i subst in
+ flexible_arg subst t
+ with Not_found -> true)
+ | _ -> false
+;;
+
+let flexible subst l = List.exists (flexible_arg subst) l;;
+
+let in_scope_tag = "tag:in_scope" ;;
+let out_scope_tag_prefix = "tag:out_scope:"
+let out_scope_tag n = out_scope_tag_prefix ^ string_of_int n ;;
+let is_out_scope_tag tag =
+ String.length tag > String.length out_scope_tag_prefix &&
+ String.sub tag 0 (String.length out_scope_tag_prefix) = out_scope_tag_prefix
+;;
+let int_of_out_scope_tag tag =
+ int_of_string
+ (String.sub tag (String.length out_scope_tag_prefix)
+ (String.length tag - (String.length out_scope_tag_prefix)))
+;;
+
+
+exception Found;;
+