From 4e529454022b7d2dc0c57d29c813c5801dfd438c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 16 Dec 2018 20:33:09 +0100
Subject: Fixes #9229 (Infix not robust wrt choice of variable names).

---
 interp/constrexpr_ops.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'interp/constrexpr_ops.mli')

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
-- 
cgit v1.2.3