aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic/Decidable.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Logic/Decidable.v')
-rw-r--r--theories/Logic/Decidable.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v
index 2ba7253c4..8b6054f9d 100644
--- a/theories/Logic/Decidable.v
+++ b/theories/Logic/Decidable.v
@@ -50,7 +50,7 @@ Qed.
Theorem dec_iff :
forall A B:Prop, decidable A -> decidable B -> decidable (A<->B).
Proof.
-unfold decidable; tauto.
+unfold decidable. tauto.
Qed.
Theorem not_not : forall P:Prop, decidable P -> ~ ~ P -> P.