Commit c285069d authored by Robbert Krebbers's avatar Robbert Krebbers

Fix compilation of algebra/auth in Coq 8.6

The rewrite auth_validN_eq was not performed in the hypothesis. It
used to work in 8.5 because of magic.
parent b7a8a0cc
......@@ -155,7 +155,7 @@ Proof.
- intros [[[?|]|] ?]; rewrite /= ?auth_valid_eq
?auth_validN_eq /= ?cmra_included_includedN ?cmra_valid_validN;
naive_solver eauto using O.
- intros n [[[]|] ?] ?; rewrite auth_validN_eq;
- intros n [[[]|] ?]; rewrite !auth_validN_eq /=;
naive_solver eauto using cmra_includedN_S, cmra_validN_S.
- by split; simpl; rewrite assoc.
- by split; simpl; rewrite comm.
......
Markdown is supported
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