diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-09-22 14:58:31 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-09-22 14:58:31 -0400 |
| commit | 550203274567b0dc4b55b31730d483f1b0f11b92 (patch) | |
| tree | 215e9e0d5c593529a529077877ace8f26b860055 | |
| parent | 38453e99a78882bf901dd3496c30fa9537483c68 (diff) | |
Revert "Fix LockedLet"
This reverts commit e9fb194f228321f9477a26bf18617047722fd42a.
| -rw-r--r-- | src/Util/LockedLet.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/LockedLet.v b/src/Util/LockedLet.v index 386b1789c..088e914fb 100644 --- a/src/Util/LockedLet.v +++ b/src/Util/LockedLet.v @@ -1,7 +1,7 @@ (** * A version of [let] that doesn't disappear under βδζ unless you also have ι and remove opacity *) Require Import Crypto.Util.Notations. -Definition locked_let {A} (x : A) : bool * A := let y := x in (true, y). +Definition locked_let {A} (x : A) : bool * A := (true, x). Definition unlock_let {A} (x : A) : locked_let x = (true, x) := eq_refl. Global Opaque locked_let. Global Arguments locked_let : simpl never. |