diff options
| author | Pierre-Marie Pédrot | 2018-12-19 16:26:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-12-19 16:26:45 +0100 |
| commit | c3e9f5f8804c3b1da323cb0a7ba7d1e46ccf0849 (patch) | |
| tree | 46e5f4fe06c02c86bff4550a4d8fd94ef12a406d /interp | |
| parent | 116f255bb51a8186a1986e5147c09a7129692af9 (diff) | |
| parent | 4e529454022b7d2dc0c57d29c813c5801dfd438c (diff) | |
Merge PR #9231: Fixes #9229: Infix not robust wrt choice of variable names in right-hand side
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr_ops.ml | 8 | ||||
| -rw-r--r-- | interp/constrexpr_ops.mli | 3 |
2 files changed, 11 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 *) diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 7f14eb4583..8c735edfc9 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -119,6 +119,9 @@ val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t val free_vars_of_constr_expr : constr_expr -> Id.Set.t val occur_var_constr_expr : Id.t -> constr_expr -> bool +(** Return all (non-qualified) names treating binders as names *) +val names_of_constr_expr : constr_expr -> Id.Set.t + val split_at_annot : local_binder_expr list -> lident option -> local_binder_expr list * local_binder_expr list val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> notation -> (int * int) list |