diff --git a/iris/proofmode/proofmode.v b/iris/proofmode/proofmode.v index f22582b198b3721d4cfe424404c4f9c884ffc481..87ea29a1489e511721837715f21d1eaef0f09bff 100644 --- a/iris/proofmode/proofmode.v +++ b/iris/proofmode/proofmode.v @@ -1,4 +1,4 @@ -(** The main proofmode file taht everyone should import. +(** The main proofmode file that everyone should import. Unless you are working with the guts of the proofmode, do not import any other file from this folder! *) From iris.proofmode Require Export ltac_tactics.