Commit 74852b24 authored by Glen Mével's avatar Glen Mével
Browse files

make a Persistent instance global

parent 9daed8bb
......@@ -226,7 +226,7 @@ Section ThunkProofs.
eapply to_agree_op_valid_L, (proj1 (Cinr_valid (A:=unitR) _)). by rewrite Cinr_op.
Qed.
Local Instance Thunk'_persistent p t γv n R φ d :
Global Instance Thunk'_persistent p t γv n R φ d :
Persistent (Thunk' p t γv n R φ d).
Proof.
revert n φ. induction d ; exact _.
......
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