diff options
Diffstat (limited to 'interp/constrexpr_ops.ml')
| -rw-r--r-- | interp/constrexpr_ops.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 3a5af1dd5f..7bc5d090b4 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -366,6 +366,14 @@ let free_vars_of_constr_expr c = | c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c in aux [] Id.Set.empty c +let names_of_constr_expr c = + let vars = ref Id.Set.empty in + let rec aux () () = function + | { CAst.v = CRef (qid, _) } when qualid_is_ident qid -> + let id = qualid_basename qid in vars := Id.Set.add id !vars + | c -> fold_constr_expr_with_binders (fun a () -> vars := Id.Set.add a !vars) aux () () c + in aux () () c; !vars + let occur_var_constr_expr id c = Id.Set.mem id (free_vars_of_constr_expr c) (* Used in correctness and interface *) |