Add dlet_nd notation

This is for non-dependent [dlet]s, to help Coq's type inference

2 files changed, 3 insertions, 0 deletions

diff --git a/src/Util/LetIn.v b/src/Util/LetIn.v
index 12e1e6d43..18e763b93 100644
--- a/src/Util/LetIn.v
+++ b/src/Util/LetIn.v
@@ -5,6 +5,7 @@ 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 "'pflet' x , pf := y 'in' f" := (Let_In_pf y (fun x pf => f)).
 
diff --git a/src/Util/Notations.v b/src/Util/Notations.v
index 0f5cd9929..455d6b498 100644
--- a/src/Util/Notations.v
+++ b/src/Util/Notations.v
@@ -72,6 +72,8 @@ Reserved Notation "'llet' x := A 'in' b"
 Reserved Notation "'mlet' x := A 'in' b"
          (at level 200, b at level 200, format "'mlet'  x  :=  A  'in' '//' b").
 (* Note that making [Let] a keyword breaks the vernacular [Let] in Coq 8.4 *)
+Reserved Notation "'dlet_nd' x := y 'in' f"
+         (at level 200, f at level 200, format "'dlet_nd'  x  :=  y  'in' '//' f").
 Reserved Notation "'dlet' x := y 'in' f"
          (at level 200, f at level 200, format "'dlet'  x  :=  y  'in' '//' f").
 Reserved Notation "'pflet' x , pf := y 'in' f"