diff --git a/ProofMode.md b/ProofMode.md
index 5bb0a54405f99f8885d7511cc566f3e6e5761894..c12a0b5b7dd3dc7cf7dd59b17a9ef041258bb3ab 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -3,7 +3,7 @@ Tactic overview
 
 Many of the tactics below apply to more goals than described in this document
 since the behavior of these tactics can be tuned via instances of the type
-classes in the file [proofmode/classes](proofmode/classes). Most notable, many
+classes in the file [proofmode/classes](proofmode/classes.v). Most notable, many
 of the tactics can be applied when the to be introduced or to be eliminated
 connective appears under a later, a primitive view shift, or in the conclusion
 of a weakest precondition connective.