diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-01 21:17:58 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-01 21:17:58 -0400 |
| commit | cbb9b2edc9fe45a0f140f1d721e5476a07430258 (patch) | |
| tree | 6a8de824972931befed95818a0b495c5e6814133 /src | |
| parent | 5e9ca7f697e4fe2c1f6b03ea2cb2fff7d760d697 (diff) | |
Fix a name (sprurious interp)
Diffstat (limited to 'src')
| -rw-r--r-- | src/Reflection/RewriterWf.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Reflection/RewriterWf.v b/src/Reflection/RewriterWf.v index f44832d29..a9ad229a0 100644 --- a/src/Reflection/RewriterWf.v +++ b/src/Reflection/RewriterWf.v @@ -43,7 +43,7 @@ Section language. Qed. End with_var. - Lemma Wf_InterpRewriteOp + Lemma Wf_RewriteOp {rewrite_op_expr} (Hrewrite_wff : forall var1 var2 G src dst opc args1 args2, wff G args1 args2 @@ -58,4 +58,4 @@ Section language. Qed. End language. -Hint Resolve Wf_InterpRewriteOp : wf. +Hint Resolve Wf_RewriteOp : wf. |