aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Util/Option.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Util/Option.v b/src/Util/Option.v
index 5feaf5e8a..ccbf6cff3 100644
--- a/src/Util/Option.v
+++ b/src/Util/Option.v
@@ -5,6 +5,7 @@ Require Import Crypto.Util.Tactics.DestructHead.
Require Import Crypto.Util.Notations.
Scheme Equality for option.
+Arguments option_beq {_} _ _ _.
Definition bind {A B} (v : option A) (f : A -> option B) : option B
:= match v with