aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/RewriterWf.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Reflection/RewriterWf.v')
-rw-r--r--src/Reflection/RewriterWf.v4
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.