Commit a4ee4c0d authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix link in

parent a47465bd
......@@ -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.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment