aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/InterpProofs.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-04-02 00:18:29 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-04-02 00:18:29 -0400
commit2882da783bf4a45cbdab2ff53d6acaea74c71f22 (patch)
tree680b491529e320e341fe7f63d573d721cb47d931 /src/Reflection/InterpProofs.v
parent7b25cca4e82d030e56fea0bebf5b7322f86e265a (diff)
Add reflective_interp rewrite db
Diffstat (limited to 'src/Reflection/InterpProofs.v')
-rw-r--r--src/Reflection/InterpProofs.v3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Reflection/InterpProofs.v b/src/Reflection/InterpProofs.v
index b0aa20ccf..a9ecdd674 100644
--- a/src/Reflection/InterpProofs.v
+++ b/src/Reflection/InterpProofs.v
@@ -60,3 +60,6 @@ Section language.
subst; eapply interpf_SmartVarVarf; eassumption.
Qed.
End language.
+
+Hint Rewrite @interpf_LetIn @interpf_SmartVarf : reflective_interp.
+Hint Rewrite @interpf_SmartVarVarf using assumption : reflective_interp.