From c285069d6dd4dbf78a9745d16507770ebaa9f9e8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 29 Nov 2016 15:39:33 +0100
Subject: [PATCH] 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.
---
algebra/auth.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/algebra/auth.v b/algebra/auth.v
index 0e757ac9e..da3d67f85 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -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.
--
GitLab