- | Some tag when tag = in_scope_tag -> 0
- | Some tag when is_out_scope_tag tag -> int_of_out_scope_tag tag
- | _ -> in_scope
+ | Some tag when tag = in_scope_tag -> 0, true
+ | Some tag when is_out_scope_tag tag->int_of_out_scope_tag tag,true
+ | _ -> in_scope, false
+ in
+ let ms =
+ if not clear then ms
+ else
+ metasenv,
+ (i,(None,c,t,ty)) :: List.filter (fun j,_ -> i <> j) subst