Commit 95b3911c authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Use strong framing for pure stuff.

parent 9578026e
......@@ -177,7 +177,8 @@ Local Ltac iFrameFinish :=
Local Ltac iFramePure t :=
let φ := type of t in
eapply (tac_frame_pure _ _ _ _ t);
[apply _ || fail "iFrame: cannot frame" φ
[typeclasses eauto with typeclass_instances strong_frame
|| fail "iFrame: cannot frame" φ
|iFrameFinish].
Local Ltac iFrameHyp strong H :=
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment