From 8c6092e8c43a74a8a175a532580284124c06e34f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
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/tacinterp.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

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

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index fd75862c6..1a8ec6d6f 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1397,9 +1397,9 @@ and tactic_of_value ist vle =
 and interp_letrec ist llc u =
   Proofview.tclUNIT () >>= fun () -> (* delay for the effects of [lref], just in case. *)
   let lref = ref ist.lfun in
-  let fold accu ((_, id), b) =
+  let fold accu ((_, na), b) =
     let v = of_tacvalue (VRec (lref, TacArg (Loc.tag b))) in
-    Id.Map.add id v accu
+    Name.fold_right (fun id -> Id.Map.add id v) na accu
   in
   let lfun = List.fold_left fold ist.lfun llc in
   let () = lref := lfun in
@@ -1412,9 +1412,9 @@ and interp_letin ist llc u =
   | [] ->
     let ist = { ist with lfun } in
     val_interp ist u
-  | ((_, id), body) :: defs ->
+  | ((_, na), body) :: defs ->
     Ftactic.bind (interp_tacarg ist body) (fun v ->
-    fold (Id.Map.add id v lfun) defs)
+    fold (Name.fold_right (fun id -> Id.Map.add id v) na lfun) defs)
   in
   fold ist.lfun llc
 
-- 
cgit v1.2.3