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.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'interp/constrexpr_ops.ml')

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