1 files changed, 3 insertions, 0 deletions
diff --git a/src/RewriterWf1.v b/src/RewriterWf1.v
index e22c8155b..420b5dc90 100644
--- a/src/RewriterWf1.v
+++ b/src/RewriterWf1.v
@@ -2571,6 +2571,9 @@ Module Compilers.
       End with_var.
     End Compile.
 
+    (** Now we prove the [wf] properties about definitions used only
+       in reification of rewrite rules, which are used to make proving
+       [wf] of concrete rewrite rules easier. *)
     Module Reify.
       Import Compile.
       Import Rewriter.Compilers.RewriteRules.Compile.