diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-03-31 09:35:54 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-03-31 09:36:16 -0400 |
| commit | 25761f294d165487bec8832272c58dae82038b95 (patch) | |
| tree | 8d7003035213995ce958079b79af95858cdc0804 /src/RewriterWf1.v | |
| parent | 8a0fc29222cd90a2c33014d4bed754241e8fdd59 (diff) | |
Add some comments based on CR requests
Diffstat (limited to 'src/RewriterWf1.v')
| -rw-r--r-- | src/RewriterWf1.v | 3 |
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. |