aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Bool
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Bool')
-rw-r--r--theories/Bool/Sumbool.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v
index 73a092143..24b6a7760 100644
--- a/theories/Bool/Sumbool.v
+++ b/theories/Bool/Sumbool.v
@@ -66,4 +66,4 @@ Definition bool_of_sumbool :
intros A B H.
elim H; intro; [exists true | exists false]; assumption.
Defined.
-Implicit Arguments bool_of_sumbool.
+Arguments bool_of_sumbool : default implicits.