From 342b79a478ed15cc42a772fcc5723d6db20c6818 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 11 Nov 2017 01:15:54 +0100
Subject: [PATCH] Bump stdpp.
---
opam | 2 +-
theories/algebra/big_op.v | 12 ++++++------
theories/algebra/cmra.v | 14 +++++++-------
theories/algebra/dra.v | 2 +-
theories/base_logic/deprecated.v | 6 +++---
theories/base_logic/double_negation.v | 2 +-
theories/base_logic/lib/fancy_updates.v | 4 ++--
theories/base_logic/lib/namespaces.v | 4 ++--
theories/base_logic/lib/viewshifts.v | 4 ++--
theories/base_logic/primitive.v | 6 +++---
theories/base_logic/upred.v | 8 ++++----
theories/program_logic/hoare.v | 8 ++++----
theories/program_logic/weakestpre.v | 8 ++++----
theories/proofmode/notation.v | 8 ++++----
14 files changed, 44 insertions(+), 44 deletions(-)
diff --git a/opam b/opam
index e3f1c66f6..ff049a508 100644
--- a/opam
+++ b/opam
@@ -12,5 +12,5 @@ remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { >= "8.6.1" & < "8.8~" }
"coq-mathcomp-ssreflect" { (>= "1.6.1" & < "1.7~") | (= "dev") }
- "coq-stdpp" { (= "dev.2017-10-28.7") | (= "dev") }
+ "coq-stdpp" { (= "dev.2017-11-11.0") | (= "dev") }
]
diff --git a/theories/algebra/big_op.v b/theories/algebra/big_op.v
index a18c18aeb..3729d5f48 100644
--- a/theories/algebra/big_op.v
+++ b/theories/algebra/big_op.v
@@ -30,10 +30,10 @@ Arguments big_opL {M} o {_ A} _ !_ /.
Typeclasses Opaque big_opL.
Notation "'[^' o 'list]' k ↦ x ∈ l , P" := (big_opL o (λ k x, P) l)
(at level 200, o at level 1, l at level 10, k, x at level 1, right associativity,
- format "[^ o list] k ↦ x ∈ l , P") : C_scope.
+ format "[^ o list] k ↦ x ∈ l , P") : stdpp_scope.
Notation "'[^' o 'list]' x ∈ l , P" := (big_opL o (λ _ x, P) l)
(at level 200, o at level 1, l at level 10, x at level 1, right associativity,
- format "[^ o list] x ∈ l , P") : C_scope.
+ format "[^ o list] x ∈ l , P") : stdpp_scope.
Definition big_opM `{Monoid M o} `{Countable K} {A} (f : K → A → M)
(m : gmap K A) : M := big_opL o (λ _, curry f) (map_to_list m).
@@ -42,10 +42,10 @@ Arguments big_opM {M} o {_ K _ _ A} _ _ : simpl never.
Typeclasses Opaque big_opM.
Notation "'[^' o 'map]' k ↦ x ∈ m , P" := (big_opM o (λ k x, P) m)
(at level 200, o at level 1, m at level 10, k, x at level 1, right associativity,
- format "[^ o map] k ↦ x ∈ m , P") : C_scope.
+ format "[^ o map] k ↦ x ∈ m , P") : stdpp_scope.
Notation "'[^' o 'map]' x ∈ m , P" := (big_opM o (λ _ x, P) m)
(at level 200, o at level 1, m at level 10, x at level 1, right associativity,
- format "[^ o map] x ∈ m , P") : C_scope.
+ format "[^ o map] x ∈ m , P") : stdpp_scope.
Definition big_opS `{Monoid M o} `{Countable A} (f : A → M)
(X : gset A) : M := big_opL o (λ _, f) (elements X).
@@ -54,7 +54,7 @@ Arguments big_opS {M} o {_ A _ _} _ _ : simpl never.
Typeclasses Opaque big_opS.
Notation "'[^' o 'set]' x ∈ X , P" := (big_opS o (λ x, P) X)
(at level 200, o at level 1, X at level 10, x at level 1, right associativity,
- format "[^ o set] x ∈ X , P") : C_scope.
+ format "[^ o set] x ∈ X , P") : stdpp_scope.
Definition big_opMS `{Monoid M o} `{Countable A} (f : A → M)
(X : gmultiset A) : M := big_opL o (λ _, f) (elements X).
@@ -63,7 +63,7 @@ Arguments big_opMS {M} o {_ A _ _} _ _ : simpl never.
Typeclasses Opaque big_opMS.
Notation "'[^' o 'mset]' x ∈ X , P" := (big_opMS o (λ x, P) X)
(at level 200, o at level 1, X at level 10, x at level 1, right associativity,
- format "[^ o mset] x ∈ X , P") : C_scope.
+ format "[^ o mset] x ∈ X , P") : stdpp_scope.
(** * Properties about big ops *)
Section big_op.
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index b6c22f5ba..3c3b1171c 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -8,8 +8,8 @@ Instance: Params (@pcore) 2.
Class Op (A : Type) := op : A → A → A.
Hint Mode Op ! : typeclass_instances.
Instance: Params (@op) 2.
-Infix "â‹…" := op (at level 50, left associativity) : C_scope.
-Notation "(â‹…)" := op (only parsing) : C_scope.
+Infix "â‹…" := op (at level 50, left associativity) : stdpp_scope.
+Notation "(â‹…)" := op (only parsing) : stdpp_scope.
(* The inclusion quantifies over [A], not [option A]. This means we do not get
reflexivity. However, if we used [option A], the following would no longer
@@ -17,8 +17,8 @@ Notation "(â‹…)" := op (only parsing) : C_scope.
x ≼ y ↔ x.1 ≼ y.1 ∧ x.2 ≼ y.2
*)
Definition included `{Equiv A, Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
-Infix "≼" := included (at level 70) : C_scope.
-Notation "(≼)" := included (only parsing) : C_scope.
+Infix "≼" := included (at level 70) : stdpp_scope.
+Notation "(≼)" := included (only parsing) : stdpp_scope.
Hint Extern 0 (_ ≼ _) => reflexivity.
Instance: Params (@included) 3.
@@ -31,11 +31,11 @@ Notation "✓{ n } x" := (validN n x)
Class Valid (A : Type) := valid : A → Prop.
Hint Mode Valid ! : typeclass_instances.
Instance: Params (@valid) 2.
-Notation "✓ x" := (valid x) (at level 20) : C_scope.
+Notation "✓ x" := (valid x) (at level 20) : stdpp_scope.
Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x ⋅ z.
Notation "x ≼{ n } y" := (includedN n x y)
- (at level 70, n at next level, format "x ≼{ n } y") : C_scope.
+ (at level 70, n at next level, format "x ≼{ n } y") : stdpp_scope.
Instance: Params (@includedN) 4.
Hint Extern 0 (_ ≼{_} _) => reflexivity.
@@ -140,7 +140,7 @@ End cmra_mixin.
Definition opM {A : cmraT} (x : A) (my : option A) :=
match my with Some y => x â‹… y | None => x end.
-Infix "â‹…?" := opM (at level 50, left associativity) : C_scope.
+Infix "â‹…?" := opM (at level 50, left associativity) : stdpp_scope.
(** * CoreId elements *)
Class CoreId {A : cmraT} (x : A) := core_id : pcore x ≡ Some x.
diff --git a/theories/algebra/dra.v b/theories/algebra/dra.v
index fcbccb2a2..dc459baf4 100644
--- a/theories/algebra/dra.v
+++ b/theories/algebra/dra.v
@@ -199,7 +199,7 @@ Proof. split; naive_solver eauto using dra_op_valid. Qed.
(* TODO: This has to be proven again. *)
(*
Lemma to_validity_included x y:
- (✓ y ∧ to_validity x ≼ to_validity y)%C ↔ (✓ x ∧ x ≼ y).
+ (✓ y ∧ to_validity x ≼ to_validity y)%stdpp ↔ (✓ x ∧ x ≼ y).
Proof.
split.
- move=>[Hvl [z [Hvxz EQ]]]. move:(Hvl)=>Hvl'. apply Hvxz in Hvl'.
diff --git a/theories/base_logic/deprecated.v b/theories/base_logic/deprecated.v
index 90180e673..3a3b9c862 100644
--- a/theories/base_logic/deprecated.v
+++ b/theories/base_logic/deprecated.v
@@ -2,11 +2,11 @@ From iris.base_logic Require Import primitive.
Set Default Proof Using "Type".
(* Deprecated 2016-11-22. Use ⌜φ⌠instead. *)
-Notation "■φ" := (uPred_pure φ%C%type)
+Notation "■φ" := (uPred_pure φ%stdpp%type)
(at level 20, right associativity, only parsing) : uPred_scope.
(* Deprecated 2016-11-22. Use ⌜x = y⌠instead. *)
-Notation "x = y" := (uPred_pure (x%C%type = y%C%type)) (only parsing) : uPred_scope.
+Notation "x = y" := (uPred_pure (x%stdpp%type = y%stdpp%type)) (only parsing) : uPred_scope.
(* Deprecated 2016-11-22. Use ⌜x ## y ⌠instead. *)
-Notation "x ## y" := (uPred_pure (x%C%type ## y%C%type)) (only parsing) : uPred_scope.
+Notation "x ## y" := (uPred_pure (x%stdpp%type ## y%stdpp%type)) (only parsing) : uPred_scope.
diff --git a/theories/base_logic/double_negation.v b/theories/base_logic/double_negation.v
index 38754d614..a27253cd1 100644
--- a/theories/base_logic/double_negation.v
+++ b/theories/base_logic/double_negation.v
@@ -9,7 +9,7 @@ Definition uPred_nnupd {M} (P: uPred M) : uPred M :=
Notation "|=n=> Q" := (uPred_nnupd Q)
(at level 99, Q at level 200, format "|=n=> Q") : uPred_scope.
Notation "P =n=> Q" := (P ⊢ |=n=> Q)
- (at level 99, Q at level 200, only parsing) : C_scope.
+ (at level 99, Q at level 200, only parsing) : stdpp_scope.
Notation "P =n=∗ Q" := (P -∗ |=n=> Q)%I
(at level 99, Q at level 200, format "P =n=∗ Q") : uPred_scope.
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 5b5cd98d8..cdc57057a 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -24,7 +24,7 @@ Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)%I
(at level 99, E1,E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }=∗ Q") : uPred_scope.
Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)
- (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : C_scope.
+ (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
Notation "|={ E }=> Q" := (fupd E E Q)
(at level 99, E at level 50, Q at level 200,
@@ -33,7 +33,7 @@ Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)%I
(at level 99, E at level 50, Q at level 200,
format "P ={ E }=∗ Q") : uPred_scope.
Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)
- (at level 99, E at level 50, Q at level 200, only parsing) : C_scope.
+ (at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope.
Section fupd.
Context `{invG Σ}.
diff --git a/theories/base_logic/lib/namespaces.v b/theories/base_logic/lib/namespaces.v
index 76857b335..dc226f276 100644
--- a/theories/base_logic/lib/namespaces.v
+++ b/theories/base_logic/lib/namespaces.v
@@ -21,8 +21,8 @@ Instance nclose : UpClose namespace coPset := unseal nclose_aux.
Definition nclose_eq : @nclose = @nclose_def := seal_eq nclose_aux.
Notation "N .@ x" := (ndot N x)
- (at level 19, left associativity, format "N .@ x") : C_scope.
-Notation "(.@)" := ndot (only parsing) : C_scope.
+ (at level 19, left associativity, format "N .@ x") : stdpp_scope.
+Notation "(.@)" := ndot (only parsing) : stdpp_scope.
Instance ndisjoint : Disjoint namespace := λ N1 N2, nclose N1 ## nclose N2.
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index a77383a45..c8ab4eb42 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -16,10 +16,10 @@ Notation "P ={ E }=> Q" := (P ={E,E}=> Q)%I
Notation "P ={ E1 , E2 }=> Q" := (P ={E1,E2}=> Q)%I
(at level 99, E1,E2 at level 50, Q at level 200,
- format "P ={ E1 , E2 }=> Q") : C_scope.
+ format "P ={ E1 , E2 }=> Q") : stdpp_scope.
Notation "P ={ E }=> Q" := (P ={E}=> Q)%I
(at level 99, E at level 50, Q at level 200,
- format "P ={ E }=> Q") : C_scope.
+ format "P ={ E }=> Q") : stdpp_scope.
Section vs.
Context `{invG Σ}.
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 3aab1eeb2..6796f5a44 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -168,7 +168,7 @@ Definition uPred_bupd {M} := unseal uPred_bupd_aux M.
Definition uPred_bupd_eq : @uPred_bupd = @uPred_bupd_def := seal_eq uPred_bupd_aux.
(* Latest notation *)
-Notation "'⌜' φ 'âŒ'" := (uPred_pure φ%C%type)
+Notation "'⌜' φ 'âŒ'" := (uPred_pure φ%stdpp%type)
(at level 1, φ at level 200, format "⌜ φ âŒ") : uPred_scope.
Notation "'False'" := (uPred_pure False) : uPred_scope.
Notation "'True'" := (uPred_pure True) : uPred_scope.
@@ -198,7 +198,7 @@ Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : uPred_scope.
Notation "|==> Q" := (uPred_bupd Q)
(at level 99, Q at level 200, format "|==> Q") : uPred_scope.
Notation "P ==∗ Q" := (P ⊢ |==> Q)
- (at level 99, Q at level 200, only parsing) : C_scope.
+ (at level 99, Q at level 200, only parsing) : stdpp_scope.
Notation "P ==∗ Q" := (P -∗ |==> Q)%I
(at level 99, Q at level 200, format "P ==∗ Q") : uPred_scope.
@@ -206,7 +206,7 @@ Coercion uPred_valid {M} (P : uPred M) : Prop := True%I ⊢ P.
Typeclasses Opaque uPred_valid.
Notation "P -∗ Q" := (P ⊢ Q)
- (at level 99, Q at level 200, right associativity) : C_scope.
+ (at level 99, Q at level 200, right associativity) : stdpp_scope.
Module uPred.
Definition unseal_eqs :=
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 801608cd7..13fc467c4 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -158,11 +158,11 @@ Hint Resolve uPred_mono uPred_closed : uPred_def.
(** Notations *)
Notation "P ⊢ Q" := (uPred_entails P%I Q%I)
- (at level 99, Q at level 200, right associativity) : C_scope.
-Notation "(⊢)" := uPred_entails (only parsing) : C_scope.
+ (at level 99, Q at level 200, right associativity) : stdpp_scope.
+Notation "(⊢)" := uPred_entails (only parsing) : stdpp_scope.
Notation "P ⊣⊢ Q" := (equiv (A:=uPred _) P%I Q%I)
- (at level 95, no associativity) : C_scope.
-Notation "(⊣⊢)" := (equiv (A:=uPred _)) (only parsing) : C_scope.
+ (at level 95, no associativity) : stdpp_scope.
+Notation "(⊣⊢)" := (equiv (A:=uPred _)) (only parsing) : stdpp_scope.
Module uPred.
Section entails.
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index cb110957a..78bc87828 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -10,17 +10,17 @@ Instance: Params (@ht) 4.
Notation "{{ P } } e @ E {{ Φ } }" := (ht E P%I e%E Φ%I)
(at level 20, P, e, Φ at level 200,
- format "{{ P } } e @ E {{ Φ } }") : C_scope.
+ format "{{ P } } e @ E {{ Φ } }") : stdpp_scope.
Notation "{{ P } } e {{ Φ } }" := (ht ⊤ P%I e%E Φ%I)
(at level 20, P, e, Φ at level 200,
- format "{{ P } } e {{ Φ } }") : C_scope.
+ format "{{ P } } e {{ Φ } }") : stdpp_scope.
Notation "{{ P } } e @ E {{ v , Q } }" := (ht E P%I e%E (λ v, Q)%I)
(at level 20, P, e, Q at level 200,
- format "{{ P } } e @ E {{ v , Q } }") : C_scope.
+ format "{{ P } } e @ E {{ v , Q } }") : stdpp_scope.
Notation "{{ P } } e {{ v , Q } }" := (ht ⊤ P%I e%E (λ v, Q)%I)
(at level 20, P, e, Q at level 200,
- format "{{ P } } e {{ v , Q } }") : C_scope.
+ format "{{ P } } e {{ v , Q } }") : stdpp_scope.
Section hoare.
Context `{irisG Λ Σ}.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 32b98d8ff..7d63d87bb 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -76,20 +76,20 @@ Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }})
(at level 20, x closed binder, y closed binder,
- format "{{{ P } } } e @ E {{{ x .. y , RET pat ; Q } } }") : C_scope.
+ format "{{{ P } } } e @ E {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }})
(at level 20, x closed binder, y closed binder,
- format "{{{ P } } } e {{{ x .. y , RET pat ; Q } } }") : C_scope.
+ format "{{{ P } } } e {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})
(at level 20,
- format "{{{ P } } } e @ E {{{ RET pat ; Q } } }") : C_scope.
+ format "{{{ P } } } e @ E {{{ RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})
(at level 20,
- format "{{{ P } } } e {{{ RET pat ; Q } } }") : C_scope.
+ format "{{{ P } } } e {{{ RET pat ; Q } } }") : stdpp_scope.
Section wp.
Context `{irisG Λ Σ}.
diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index bf7dd0f00..de56cc823 100644
--- a/theories/proofmode/notation.v
+++ b/theories/proofmode/notation.v
@@ -16,14 +16,14 @@ Notation "Γ '--------------------------------------' □ Δ '------------------
(envs_entails (Envs Γ Δ) Q%I)
(at level 1, Q at level 200, left associativity,
format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' Q '//'", only printing) :
- C_scope.
+ stdpp_scope.
Notation "Δ '--------------------------------------' ∗ Q" :=
(envs_entails (Envs Enil Δ) Q%I)
(at level 1, Q at level 200, left associativity,
- format "Δ '--------------------------------------' ∗ '//' Q '//'", only printing) : C_scope.
+ format "Δ '--------------------------------------' ∗ '//' Q '//'", only printing) : stdpp_scope.
Notation "Γ '--------------------------------------' □ Q" :=
(envs_entails (Envs Γ Enil) Q%I)
(at level 1, Q at level 200, left associativity,
- format "Γ '--------------------------------------' □ '//' Q '//'", only printing) : C_scope.
+ format "Γ '--------------------------------------' □ '//' Q '//'", only printing) : stdpp_scope.
Notation "'--------------------------------------' ∗ Q" := (envs_entails (Envs Enil Enil) Q%I)
- (at level 1, Q at level 200, format "'--------------------------------------' ∗ '//' Q '//'", only printing) : C_scope.
+ (at level 1, Q at level 200, format "'--------------------------------------' ∗ '//' Q '//'", only printing) : stdpp_scope.
--
GitLab