Support destructuring dlet and slet

The current way to support it is a kludge around the fact that `x
binder` only works for recursive notations

1 files changed, 3 insertions, 3 deletions

diff --git a/src/Util/LetIn.v b/src/Util/LetIn.v
index 69cacd75e..92c7b51ad 100644
--- a/src/Util/LetIn.v
+++ b/src/Util/LetIn.v
@@ -5,12 +5,12 @@ Require Import Crypto.Util.Notations.
 
 Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y.
 Definition Let_In_pf {A P} (x : A) (f : forall a : A, a = x -> P a) : P x := let y := x in f y eq_refl.
-Notation "'dlet_nd' x := y 'in' f" := (Let_In (P:=fun _ => _) y (fun x => f)) (only parsing).
-Notation "'dlet' x := y 'in' f" := (Let_In y (fun x => f)).
+Notation "'dlet_nd' x .. y := v 'in' f" := (Let_In (P:=fun _ => _) v (fun x => .. (fun y => f) .. )) (only parsing).
+Notation "'dlet' x .. y := v 'in' f" := (Let_In v (fun x => .. (fun y => f) .. )).
 Notation "'pflet' x , pf := y 'in' f" := (Let_In_pf y (fun x pf => f)).
 
 Module Bug5107WorkAround.
-  Notation "'dlet' x := y 'in' f" := (Let_In (P:=fun _ => _) y (fun x => f)).
+  Notation "'dlet' x .. y := v 'in' f" := (Let_In (P:=fun _ => _) v (fun x => .. (fun y => f) .. )).
 End Bug5107WorkAround.
 
 Global Instance Proper_Let_In_nd_changebody {A P R} {Reflexive_R:@Reflexive P R}