aboutsummaryrefslogtreecommitdiffstats
path: root/common/Errors.v
diff options
context:
space:
mode:
Diffstat (limited to 'common/Errors.v')
-rw-r--r--common/Errors.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/common/Errors.v b/common/Errors.v
index 293b7993..28933313 100644
--- a/common/Errors.v
+++ b/common/Errors.v
@@ -47,7 +47,7 @@ Inductive res (A: Type) : Type :=
| OK: A -> res A
| Error: errmsg -> res A.
-Implicit Arguments Error [A].
+Arguments Error [A].
(** To automate the propagation of errors, we use a monadic style
with the following [bind] operation. *)