diff options
| author | Hugo Herbelin | 2018-12-16 20:33:09 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-12-18 18:24:31 +0100 |
| commit | 4e529454022b7d2dc0c57d29c813c5801dfd438c (patch) | |
| tree | d84962c9f9dd70977f3f151610b9c4769ac2023e /interp/constrexpr_ops.mli | |
| parent | 4c733a9282bf2a272eb0ff48811b528aebbfb5a0 (diff) | |
Fixes #9229 (Infix not robust wrt choice of variable names).
Diffstat (limited to 'interp/constrexpr_ops.mli')
| -rw-r--r-- | interp/constrexpr_ops.mli | 3 |
1 files changed, 3 insertions, 0 deletions
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 |