From 8c6092e8c43a74a8a175a532580284124c06e34f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 22 Oct 2017 23:50:11 +0200
Subject: Adding support for syntax "let _ := e in e'" in Ltac.

Adding a file fixing #5996 and which uses this feature.
---
 plugins/ltac/tacintern.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'plugins/ltac/tacintern.ml')

diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index f171fd07d7..b16b0a7bae 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -468,9 +468,10 @@ let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function
 (* Utilities *)
 let extract_let_names lrc =
   let fold accu ((loc, name), _) =
-    if Id.Set.mem name accu then user_err ?loc
+    Nameops.Name.fold_right (fun id accu ->
+    if Id.Set.mem id accu then user_err ?loc
       ~hdr:"glob_tactic" (str "This variable is bound several times.")
-    else Id.Set.add name accu
+    else Id.Set.add id accu) name accu
   in
   List.fold_left fold Id.Set.empty lrc
 
@@ -812,7 +813,7 @@ let notation_subst bindings tac =
   let fold id c accu =
     let loc = Glob_ops.loc_of_glob_constr (fst c) in
     let c = ConstrMayEval (ConstrTerm c) in
-    ((loc, id), c) :: accu
+    ((loc, Name id), c) :: accu
   in
   let bindings = Id.Map.fold fold bindings [] in
   (** This is theoretically not correct due to potential variable capture, but
-- 
cgit v1.2.3