Merge commit '342b79a4' into gen_proofmode

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") }
 ]

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.

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.

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'.

theories/base_logic/deprecated.v

@@ -5,12 +5,12 @@ 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.
 *)

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") : bi_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") : bi_scope.
 

theories/base_logic/lib/fancy_updates.v

@@ -23,7 +23,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") : bi_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,
@@ -32,7 +32,7 @@ Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)%I
   (at level 99, E at level 50, Q at level 200,
    format "P  ={ E }=∗  Q") : bi_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 Σ}.

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.
 

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 Σ}.

theories/base_logic/upred.v

@@ -558,7 +558,7 @@ Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : bi_scope.
 Notation "|==> Q" := (uPred_bupd Q)
   (at level 99, Q at level 200, format "|==>  Q") : bi_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") : bi_scope.
 

theories/bi/interface.v

@@ -28,7 +28,7 @@ Section bi_mixin.
   Local Notation "'emp'" := bi_emp.
   Local Notation "'True'" := (bi_pure True).
   Local Notation "'False'" := (bi_pure False).
-  Local Notation "'⌜' φ '⌝'" := (bi_pure φ%type%C).
+  Local Notation "'⌜' φ '⌝'" := (bi_pure φ%type%stdpp).
   Local Infix "∧" := bi_and.
   Local Infix "∨" := bi_or.
   Local Infix "→" := bi_impl.
@@ -213,7 +213,7 @@ Arguments bi_dist : simpl never.
 Arguments bi_equiv : simpl never.
 Arguments bi_entails {PROP} _%I _%I : simpl never, rename.
 Arguments bi_emp {PROP} : simpl never, rename.
-Arguments bi_pure {PROP} _%C : simpl never, rename.
+Arguments bi_pure {PROP} _%stdpp : simpl never, rename.
 Arguments bi_and {PROP} _%I _%I : simpl never, rename.
 Arguments bi_or {PROP} _%I _%I : simpl never, rename.
 Arguments bi_impl {PROP} _%I _%I : simpl never, rename.
@@ -255,7 +255,7 @@ Structure sbi := SBI {
 Arguments sbi_car : simpl never.
 Arguments sbi_entails {PROP} _%I _%I : simpl never, rename.
 Arguments bi_emp {PROP} : simpl never, rename.
-Arguments bi_pure {PROP} _%C : simpl never, rename.
+Arguments bi_pure {PROP} _%stdpp : simpl never, rename.
 Arguments bi_and {PROP} _%I _%I : simpl never, rename.
 Arguments bi_or {PROP} _%I _%I : simpl never, rename.
 Arguments bi_impl {PROP} _%I _%I : simpl never, rename.
@@ -278,7 +278,7 @@ Arguments sbi_dist : simpl never.
 Arguments sbi_equiv : simpl never.
 Arguments sbi_entails {PROP} _%I _%I : simpl never, rename.
 Arguments sbi_emp {PROP} : simpl never, rename.
-Arguments sbi_pure {PROP} _%C : simpl never, rename.
+Arguments sbi_pure {PROP} _%stdpp : simpl never, rename.
 Arguments sbi_and {PROP} _%I _%I : simpl never, rename.
 Arguments sbi_or {PROP} _%I _%I : simpl never, rename.
 Arguments sbi_impl {PROP} _%I _%I : simpl never, rename.
@@ -295,17 +295,17 @@ Hint Extern 0 (bi_entails _ _) => reflexivity.
 Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP).
 Instance bi_inhabited {PROP : bi} : Inhabited PROP := populate (bi_pure True).
 
-Notation "P ⊢ Q" := (bi_entails P%I Q%I) : C_scope.
-Notation "(⊢)" := bi_entails (only parsing) : C_scope.
+Notation "P ⊢ Q" := (bi_entails P%I Q%I) : stdpp_scope.
+Notation "(⊢)" := bi_entails (only parsing) : stdpp_scope.
 
 Notation "P ⊣⊢ Q" := (equiv (A:=bi_car _) P%I Q%I)
-  (at level 95, no associativity) : C_scope.
-Notation "(⊣⊢)" := (equiv (A:=bi_car _)) (only parsing) : C_scope.
+  (at level 95, no associativity) : stdpp_scope.
+Notation "(⊣⊢)" := (equiv (A:=bi_car _)) (only parsing) : stdpp_scope.
 
-Notation "P -∗ Q" := (P ⊢ Q) : C_scope.
+Notation "P -∗ Q" := (P ⊢ Q) : stdpp_scope.
 
 Notation "'emp'" := (bi_emp) : bi_scope.
-Notation "'⌜' φ '⌝'" := (bi_pure φ%type%C) : bi_scope.
+Notation "'⌜' φ '⌝'" := (bi_pure φ%type%stdpp) : bi_scope.
 Notation "'True'" := (bi_pure True) : bi_scope.
 Notation "'False'" := (bi_pure False) : bi_scope.
 Infix "∧" := bi_and : bi_scope.

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 Λ Σ}.

theories/program_logic/weakestpre.v

@@ -75,20 +75,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 Λ Σ}.

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.