Change [Let ... in ...] to [dlet ... in ...] (#67)

For "definition".  This fixes #65; [Let] conflicts with the vernacular
[Let] in Coq 8.4.

2 files changed, 4 insertions, 3 deletions

diff --git a/src/Util/LetIn.v b/src/Util/LetIn.v
index a15204c96..d94674f2f 100644
--- a/src/Util/LetIn.v
+++ b/src/Util/LetIn.v
@@ -3,7 +3,7 @@ Require Import Crypto.Util.Tactics.
 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.
-Notation "'Let' x := y 'in' f" := (Let_In y (fun x => f)).
+Notation "'dlet' x := y 'in' f" := (Let_In y (fun x => f)).
 
 Global Instance Proper_Let_In_nd_changebody {A P R} {Reflexive_R:@Reflexive P R}
   : Proper (eq ==> pointwise_relation _ R ==> R) (@Let_In A (fun _ => P)).
diff --git a/src/Util/Notations.v b/src/Util/Notations.v
index 1c21a6cf8..22ddf854c 100644
--- a/src/Util/Notations.v
+++ b/src/Util/Notations.v
@@ -63,7 +63,8 @@ Reserved Notation "'plet' x := y 'in' z"
          (at level 200, z at level 200, format "'plet'  x  :=  y  'in' '//' z").
 Reserved Notation "'slet' x := A 'in' b"
          (at level 200, b at level 200, format "'slet'  x  :=  A  'in' '//' b").
-Reserved Notation "'Let' x := y 'in' f"
-         (at level 200, f at level 200, format "'Let'  x  :=  y  'in' '//' f").
+(* Note that making [Let] a keyword breaks the vernacular [Let] in Coq 8.4 *)
+Reserved Notation "'dlet' x := y 'in' f"
+         (at level 200, f at level 200, format "'dlet'  x  :=  y  'in' '//' f").
 Reserved Notation "'λ'  x .. y , t" (at level 200, x binder, y binder, right associativity).
 Reserved Notation "'λn'  x .. y , t" (at level 200, right associativity).