From b0e11cff023812ed4bc64cc7d5888b2b45927024 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 17 Aug 2017 19:06:40 +0200
Subject: [PATCH] Bump coq-stdpp.
---
opam.pins | 2 +-
theories/algebra/auth.v | 3 ++-
theories/algebra/ofe.v | 11 ++++++-----
3 files changed, 9 insertions(+), 7 deletions(-)
diff --git a/opam.pins b/opam.pins
index c16dcc84e..d9fa24e4f 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp ee6200b4d74bfd06034f3cc36d1afdc309427e5c
+coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 24cc2e4786b2344e092e412f56e96c6971ab60d8
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index c410171fe..c49bfa240 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -279,7 +279,8 @@ Proof.
split; try apply _.
- intros n [[[a|]|] b]; rewrite !auth_validN_eq; try
naive_solver eauto using cmra_morphism_monotoneN, cmra_morphism_validN.
- - intros [??]. apply Some_proper. by f_equiv; rewrite /= cmra_morphism_core.
+ - intros [??]. apply Some_proper; rewrite /auth_map /=.
+ by f_equiv; rewrite /= cmra_morphism_core.
- intros [[?|]?] [[?|]?]; try apply Auth_proper=>//=; by rewrite cmra_morphism_op.
Qed.
Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 1796ace9e..ce44a5526 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -239,17 +239,18 @@ End contractive.
Ltac f_contractive :=
match goal with
- | |- ?f _ ≡{_}≡ ?f _ => apply (_ : Proper (dist_later _ ==> _) f)
- | |- ?f _ _ ≡{_}≡ ?f _ _ => apply (_ : Proper (dist_later _ ==> _ ==> _) f)
- | |- ?f _ _ ≡{_}≡ ?f _ _ => apply (_ : Proper (_ ==> dist_later _ ==> _) f)
+ | |- ?f _ ≡{_}≡ ?f _ => simple apply (_ : Proper (dist_later _ ==> _) f)
+ | |- ?f _ _ ≡{_}≡ ?f _ _ => simple apply (_ : Proper (dist_later _ ==> _ ==> _) f)
+ | |- ?f _ _ ≡{_}≡ ?f _ _ => simple apply (_ : Proper (_ ==> dist_later _ ==> _) f)
end;
try match goal with
| |- @dist_later ?A _ ?n ?x ?y =>
destruct n as [|n]; [exact I|change (@dist A _ n x y)]
end;
- try reflexivity.
+ try simple apply reflexivity.
-Ltac solve_contractive := solve_proper_core ltac:(fun _ => first [f_contractive | f_equiv]).
+Ltac solve_contractive :=
+ solve_proper_core ltac:(fun _ => first [f_contractive | f_equiv]).
(** Limit preserving predicates *)
Class LimitPreserving `{!Cofe A} (P : A → Prop) : Prop :=
--
GitLab