diff git a/theories/base.v b/theories/base.v
index 6f02d571db28f866a8a251f4caa11f742cea015e..d6f95cd4b32c5023fc40ead3223671dc70aa40de 100644
 a/theories/base.v
+++ b/theories/base.v
@@ 91,10 +91,10 @@ Existing Class TCForall.
Existing Instance TCForall_nil.
Existing Instance TCForall_cons.
(** Throughout this development we use [C_scope] for all general purpose
+(** Throughout this development we use [stdpp_scope] for all general purpose
notations that do not belong to a more specific scope. *)
Delimit Scope C_scope with C.
Global Open Scope C_scope.
+Delimit Scope stdpp_scope with stdpp.
+Global Open Scope stdpp_scope.
(** Change [True] and [False] into notations in order to enable overloading.
We will use this to give [True] and [False] a different interpretation for
@@ 105,12 +105,12 @@ Notation "'False'" := False : type_scope.
(** * Equality *)
(** Introduce some Haskell style like notations. *)
Notation "(=)" := eq (only parsing) : C_scope.
Notation "( x =)" := (eq x) (only parsing) : C_scope.
Notation "(= x )" := (λ y, eq y x) (only parsing) : C_scope.
Notation "(≠)" := (λ x y, x ≠ y) (only parsing) : C_scope.
Notation "( x ≠)" := (λ y, x ≠ y) (only parsing) : C_scope.
Notation "(≠ x )" := (λ y, y ≠ x) (only parsing) : C_scope.
+Notation "(=)" := eq (only parsing) : stdpp_scope.
+Notation "( x =)" := (eq x) (only parsing) : stdpp_scope.
+Notation "(= x )" := (λ y, eq y x) (only parsing) : stdpp_scope.
+Notation "(≠)" := (λ x y, x ≠ y) (only parsing) : stdpp_scope.
+Notation "( x ≠)" := (λ y, x ≠ y) (only parsing) : stdpp_scope.
+Notation "(≠ x )" := (λ y, y ≠ x) (only parsing) : stdpp_scope.
Hint Extern 0 (_ = _) => reflexivity.
Hint Extern 100 (_ ≠ _) => discriminate.
@@ 125,14 +125,14 @@ Class Equiv A := equiv: relation A.
(* No Hint Mode set because of Coq bug #5735
Hint Mode Equiv ! : typeclass_instances. *)
Infix "≡" := equiv (at level 70, no associativity) : C_scope.
Notation "(≡)" := equiv (only parsing) : C_scope.
Notation "( X ≡)" := (equiv X) (only parsing) : C_scope.
Notation "(≡ X )" := (λ Y, Y ≡ X) (only parsing) : C_scope.
Notation "(≢)" := (λ X Y, ¬X ≡ Y) (only parsing) : C_scope.
Notation "X ≢ Y":= (¬X ≡ Y) (at level 70, no associativity) : C_scope.
Notation "( X ≢)" := (λ Y, X ≢ Y) (only parsing) : C_scope.
Notation "(≢ X )" := (λ Y, Y ≢ X) (only parsing) : C_scope.
+Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope.
+Notation "(≡)" := equiv (only parsing) : stdpp_scope.
+Notation "( X ≡)" := (equiv X) (only parsing) : stdpp_scope.
+Notation "(≡ X )" := (λ Y, Y ≡ X) (only parsing) : stdpp_scope.
+Notation "(≢)" := (λ X Y, ¬X ≡ Y) (only parsing) : stdpp_scope.
+Notation "X ≢ Y":= (¬X ≡ Y) (at level 70, no associativity) : stdpp_scope.
+Notation "( X ≢)" := (λ Y, X ≢ Y) (only parsing) : stdpp_scope.
+Notation "(≢ X )" := (λ Y, Y ≢ X) (only parsing) : stdpp_scope.
(** The type class [LeibnizEquiv] collects setoid equalities that coincide
with Leibniz equality. We provide the tactic [fold_leibniz] to transform such
@@ 331,17 +331,17 @@ Class TotalOrder {A} (R : relation A) : Prop := {
}.
(** * Logic *)
Notation "(∧)" := and (only parsing) : C_scope.
Notation "( A ∧)" := (and A) (only parsing) : C_scope.
Notation "(∧ B )" := (λ A, A ∧ B) (only parsing) : C_scope.
+Notation "(∧)" := and (only parsing) : stdpp_scope.
+Notation "( A ∧)" := (and A) (only parsing) : stdpp_scope.
+Notation "(∧ B )" := (λ A, A ∧ B) (only parsing) : stdpp_scope.
Notation "(∨)" := or (only parsing) : C_scope.
Notation "( A ∨)" := (or A) (only parsing) : C_scope.
Notation "(∨ B )" := (λ A, A ∨ B) (only parsing) : C_scope.
+Notation "(∨)" := or (only parsing) : stdpp_scope.
+Notation "( A ∨)" := (or A) (only parsing) : stdpp_scope.
+Notation "(∨ B )" := (λ A, A ∨ B) (only parsing) : stdpp_scope.
Notation "(↔)" := iff (only parsing) : C_scope.
Notation "( A ↔)" := (iff A) (only parsing) : C_scope.
Notation "(↔ B )" := (λ A, A ↔ B) (only parsing) : C_scope.
+Notation "(↔)" := iff (only parsing) : stdpp_scope.
+Notation "( A ↔)" := (iff A) (only parsing) : stdpp_scope.
+Notation "(↔ B )" := (λ A, A ↔ B) (only parsing) : stdpp_scope.
Hint Extern 0 (_ ↔ _) => reflexivity.
Hint Extern 0 (_ ↔ _) => symmetry; assumption.
@@ 405,19 +405,19 @@ Proof. unfold impl. red; intuition. Qed.
(** * Common data types *)
(** ** Functions *)
Notation "(→)" := (λ A B, A → B) (only parsing) : C_scope.
Notation "( A →)" := (λ B, A → B) (only parsing) : C_scope.
Notation "(→ B )" := (λ A, A → B) (only parsing) : C_scope.
+Notation "(→)" := (λ A B, A → B) (only parsing) : stdpp_scope.
+Notation "( A →)" := (λ B, A → B) (only parsing) : stdpp_scope.
+Notation "(→ B )" := (λ A, A → B) (only parsing) : stdpp_scope.
Notation "t $ r" := (t r)
 (at level 65, right associativity, only parsing) : C_scope.
Notation "($)" := (λ f x, f x) (only parsing) : C_scope.
Notation "($ x )" := (λ f, f x) (only parsing) : C_scope.
+ (at level 65, right associativity, only parsing) : stdpp_scope.
+Notation "($)" := (λ f x, f x) (only parsing) : stdpp_scope.
+Notation "($ x )" := (λ f, f x) (only parsing) : stdpp_scope.
Infix "∘" := compose : C_scope.
Notation "(∘)" := compose (only parsing) : C_scope.
Notation "( f ∘)" := (compose f) (only parsing) : C_scope.
Notation "(∘ f )" := (λ g, compose g f) (only parsing) : C_scope.
+Infix "∘" := compose : stdpp_scope.
+Notation "(∘)" := compose (only parsing) : stdpp_scope.
+Notation "( f ∘)" := (compose f) (only parsing) : stdpp_scope.
+Notation "(∘ f )" := (λ g, compose g f) (only parsing) : stdpp_scope.
Instance impl_inhabited {A} `{Inhabited B} : Inhabited (A → B) :=
populate (λ _, inhabitant).
@@ 510,8 +510,8 @@ Proof. intros [] []; reflexivity. Qed.
Instance unit_inhabited: Inhabited unit := populate ().
(** ** Products *)
Notation "( x ,)" := (pair x) (only parsing) : C_scope.
Notation "(, y )" := (λ x, (x,y)) (only parsing) : C_scope.
+Notation "( x ,)" := (pair x) (only parsing) : stdpp_scope.
+Notation "(, y )" := (λ x, (x,y)) (only parsing) : stdpp_scope.
Notation "p .1" := (fst p) (at level 10, format "p .1").
Notation "p .2" := (snd p) (at level 10, format "p .2").
@@ 657,8 +657,8 @@ Arguments projT2 {_ _} _ : assert.
Arguments exist {_} _ _ _ : assert.
Arguments proj1_sig {_ _} _ : assert.
Arguments proj2_sig {_ _} _ : assert.
Notation "x ↾ p" := (exist _ x p) (at level 20) : C_scope.
Notation "` x" := (proj1_sig x) (at level 10, format "` x") : C_scope.
+Notation "x ↾ p" := (exist _ x p) (at level 20) : stdpp_scope.
+Notation "` x" := (proj1_sig x) (at level 10, format "` x") : stdpp_scope.
Lemma proj1_sig_inj {A} (P : A → Prop) x (Px : P x) y (Py : P y) :
x↾Px = y↾Py → x = y.
@@ 684,102 +684,102 @@ intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
[(⊆)] and element of [(∈)] relation, and disjointess [(##)]. *)
Class Empty A := empty: A.
Hint Mode Empty ! : typeclass_instances.
Notation "∅" := empty : C_scope.
+Notation "∅" := empty : stdpp_scope.
Instance empty_inhabited `(Empty A) : Inhabited A := populate ∅.
Class Top A := top : A.
Hint Mode Top ! : typeclass_instances.
Notation "⊤" := top : C_scope.
+Notation "⊤" := top : stdpp_scope.
Class Union A := union: A → A → A.
Hint Mode Union ! : typeclass_instances.
Instance: Params (@union) 2.
Infix "∪" := union (at level 50, left associativity) : C_scope.
Notation "(∪)" := union (only parsing) : C_scope.
Notation "( x ∪)" := (union x) (only parsing) : C_scope.
Notation "(∪ x )" := (λ y, union y x) (only parsing) : C_scope.
Infix "∪*" := (zip_with (∪)) (at level 50, left associativity) : C_scope.
Notation "(∪*)" := (zip_with (∪)) (only parsing) : C_scope.
+Infix "∪" := union (at level 50, left associativity) : stdpp_scope.
+Notation "(∪)" := union (only parsing) : stdpp_scope.
+Notation "( x ∪)" := (union x) (only parsing) : stdpp_scope.
+Notation "(∪ x )" := (λ y, union y x) (only parsing) : stdpp_scope.
+Infix "∪*" := (zip_with (∪)) (at level 50, left associativity) : stdpp_scope.
+Notation "(∪*)" := (zip_with (∪)) (only parsing) : stdpp_scope.
Infix "∪**" := (zip_with (zip_with (∪)))
 (at level 50, left associativity) : C_scope.
+ (at level 50, left associativity) : stdpp_scope.
Infix "∪*∪**" := (zip_with (prod_zip (∪) (∪*)))
 (at level 50, left associativity) : C_scope.
+ (at level 50, left associativity) : stdpp_scope.
Definition union_list `{Empty A} `{Union A} : list A → A := fold_right (∪) ∅.
Arguments union_list _ _ _ !_ / : assert.
Notation "⋃ l" := (union_list l) (at level 20, format "⋃ l") : C_scope.
+Notation "⋃ l" := (union_list l) (at level 20, format "⋃ l") : stdpp_scope.
Class Intersection A := intersection: A → A → A.
Hint Mode Intersection ! : typeclass_instances.
Instance: Params (@intersection) 2.
Infix "∩" := intersection (at level 40) : C_scope.
Notation "(∩)" := intersection (only parsing) : C_scope.
Notation "( x ∩)" := (intersection x) (only parsing) : C_scope.
Notation "(∩ x )" := (λ y, intersection y x) (only parsing) : C_scope.
+Infix "∩" := intersection (at level 40) : stdpp_scope.
+Notation "(∩)" := intersection (only parsing) : stdpp_scope.
+Notation "( x ∩)" := (intersection x) (only parsing) : stdpp_scope.
+Notation "(∩ x )" := (λ y, intersection y x) (only parsing) : stdpp_scope.
Class Difference A := difference: A → A → A.
Hint Mode Difference ! : typeclass_instances.
Instance: Params (@difference) 2.
Infix "∖" := difference (at level 40, left associativity) : C_scope.
Notation "(∖)" := difference (only parsing) : C_scope.
Notation "( x ∖)" := (difference x) (only parsing) : C_scope.
Notation "(∖ x )" := (λ y, difference y x) (only parsing) : C_scope.
Infix "∖*" := (zip_with (∖)) (at level 40, left associativity) : C_scope.
Notation "(∖*)" := (zip_with (∖)) (only parsing) : C_scope.
+Infix "∖" := difference (at level 40, left associativity) : stdpp_scope.
+Notation "(∖)" := difference (only parsing) : stdpp_scope.
+Notation "( x ∖)" := (difference x) (only parsing) : stdpp_scope.
+Notation "(∖ x )" := (λ y, difference y x) (only parsing) : stdpp_scope.
+Infix "∖*" := (zip_with (∖)) (at level 40, left associativity) : stdpp_scope.
+Notation "(∖*)" := (zip_with (∖)) (only parsing) : stdpp_scope.
Infix "∖**" := (zip_with (zip_with (∖)))
 (at level 40, left associativity) : C_scope.
+ (at level 40, left associativity) : stdpp_scope.
Infix "∖*∖**" := (zip_with (prod_zip (∖) (∖*)))
 (at level 50, left associativity) : C_scope.
+ (at level 50, left associativity) : stdpp_scope.
Class Singleton A B := singleton: A → B.
Hint Mode Singleton  ! : typeclass_instances.
Instance: Params (@singleton) 3.
Notation "{[ x ]}" := (singleton x) (at level 1) : C_scope.
+Notation "{[ x ]}" := (singleton x) (at level 1) : stdpp_scope.
Notation "{[ x ; y ; .. ; z ]}" :=
(union .. (union (singleton x) (singleton y)) .. (singleton z))
 (at level 1) : C_scope.
+ (at level 1) : stdpp_scope.
Notation "{[ x , y ]}" := (singleton (x,y))
 (at level 1, y at next level) : C_scope.
+ (at level 1, y at next level) : stdpp_scope.
Notation "{[ x , y , z ]}" := (singleton (x,y,z))
 (at level 1, y at next level, z at next level) : C_scope.
+ (at level 1, y at next level, z at next level) : stdpp_scope.
Class SubsetEq A := subseteq: relation A.
Hint Mode SubsetEq ! : typeclass_instances.
Instance: Params (@subseteq) 2.
Infix "⊆" := subseteq (at level 70) : C_scope.
Notation "(⊆)" := subseteq (only parsing) : C_scope.
Notation "( X ⊆)" := (subseteq X) (only parsing) : C_scope.
Notation "(⊆ X )" := (λ Y, Y ⊆ X) (only parsing) : C_scope.
Notation "X ⊈ Y" := (¬X ⊆ Y) (at level 70) : C_scope.
Notation "(⊈)" := (λ X Y, X ⊈ Y) (only parsing) : C_scope.
Notation "( X ⊈)" := (λ Y, X ⊈ Y) (only parsing) : C_scope.
Notation "(⊈ X )" := (λ Y, Y ⊈ X) (only parsing) : C_scope.
Infix "⊆*" := (Forall2 (⊆)) (at level 70) : C_scope.
Notation "(⊆*)" := (Forall2 (⊆)) (only parsing) : C_scope.
Infix "⊆**" := (Forall2 (⊆*)) (at level 70) : C_scope.
Infix "⊆1*" := (Forall2 (λ p q, p.1 ⊆ q.1)) (at level 70) : C_scope.
Infix "⊆2*" := (Forall2 (λ p q, p.2 ⊆ q.2)) (at level 70) : C_scope.
Infix "⊆1**" := (Forall2 (λ p q, p.1 ⊆* q.1)) (at level 70) : C_scope.
Infix "⊆2**" := (Forall2 (λ p q, p.2 ⊆* q.2)) (at level 70) : C_scope.
+Infix "⊆" := subseteq (at level 70) : stdpp_scope.
+Notation "(⊆)" := subseteq (only parsing) : stdpp_scope.
+Notation "( X ⊆)" := (subseteq X) (only parsing) : stdpp_scope.
+Notation "(⊆ X )" := (λ Y, Y ⊆ X) (only parsing) : stdpp_scope.
+Notation "X ⊈ Y" := (¬X ⊆ Y) (at level 70) : stdpp_scope.
+Notation "(⊈)" := (λ X Y, X ⊈ Y) (only parsing) : stdpp_scope.
+Notation "( X ⊈)" := (λ Y, X ⊈ Y) (only parsing) : stdpp_scope.
+Notation "(⊈ X )" := (λ Y, Y ⊈ X) (only parsing) : stdpp_scope.
+Infix "⊆*" := (Forall2 (⊆)) (at level 70) : stdpp_scope.
+Notation "(⊆*)" := (Forall2 (⊆)) (only parsing) : stdpp_scope.
+Infix "⊆**" := (Forall2 (⊆*)) (at level 70) : stdpp_scope.
+Infix "⊆1*" := (Forall2 (λ p q, p.1 ⊆ q.1)) (at level 70) : stdpp_scope.
+Infix "⊆2*" := (Forall2 (λ p q, p.2 ⊆ q.2)) (at level 70) : stdpp_scope.
+Infix "⊆1**" := (Forall2 (λ p q, p.1 ⊆* q.1)) (at level 70) : stdpp_scope.
+Infix "⊆2**" := (Forall2 (λ p q, p.2 ⊆* q.2)) (at level 70) : stdpp_scope.
Hint Extern 0 (_ ⊆ _) => reflexivity.
Hint Extern 0 (_ ⊆* _) => reflexivity.
Hint Extern 0 (_ ⊆** _) => reflexivity.
Infix "⊂" := (strict (⊆)) (at level 70) : C_scope.
Notation "(⊂)" := (strict (⊆)) (only parsing) : C_scope.
Notation "( X ⊂)" := (strict (⊆) X) (only parsing) : C_scope.
Notation "(⊂ X )" := (λ Y, Y ⊂ X) (only parsing) : C_scope.
Notation "X ⊄ Y" := (¬X ⊂ Y) (at level 70) : C_scope.
Notation "(⊄)" := (λ X Y, X ⊄ Y) (only parsing) : C_scope.
Notation "( X ⊄)" := (λ Y, X ⊄ Y) (only parsing) : C_scope.
Notation "(⊄ X )" := (λ Y, Y ⊄ X) (only parsing) : C_scope.
+Infix "⊂" := (strict (⊆)) (at level 70) : stdpp_scope.
+Notation "(⊂)" := (strict (⊆)) (only parsing) : stdpp_scope.
+Notation "( X ⊂)" := (strict (⊆) X) (only parsing) : stdpp_scope.
+Notation "(⊂ X )" := (λ Y, Y ⊂ X) (only parsing) : stdpp_scope.
+Notation "X ⊄ Y" := (¬X ⊂ Y) (at level 70) : stdpp_scope.
+Notation "(⊄)" := (λ X Y, X ⊄ Y) (only parsing) : stdpp_scope.
+Notation "( X ⊄)" := (λ Y, X ⊄ Y) (only parsing) : stdpp_scope.
+Notation "(⊄ X )" := (λ Y, Y ⊄ X) (only parsing) : stdpp_scope.
Notation "X ⊆ Y ⊆ Z" := (X ⊆ Y ∧ Y ⊆ Z) (at level 70, Y at next level) : C_scope.
Notation "X ⊆ Y ⊂ Z" := (X ⊆ Y ∧ Y ⊂ Z) (at level 70, Y at next level) : C_scope.
Notation "X ⊂ Y ⊆ Z" := (X ⊂ Y ∧ Y ⊆ Z) (at level 70, Y at next level) : C_scope.
Notation "X ⊂ Y ⊂ Z" := (X ⊂ Y ∧ Y ⊂ Z) (at level 70, Y at next level) : C_scope.
+Notation "X ⊆ Y ⊆ Z" := (X ⊆ Y ∧ Y ⊆ Z) (at level 70, Y at next level) : stdpp_scope.
+Notation "X ⊆ Y ⊂ Z" := (X ⊆ Y ∧ Y ⊂ Z) (at level 70, Y at next level) : stdpp_scope.
+Notation "X ⊂ Y ⊆ Z" := (X ⊂ Y ∧ Y ⊆ Z) (at level 70, Y at next level) : stdpp_scope.
+Notation "X ⊂ Y ⊂ Z" := (X ⊂ Y ∧ Y ⊂ Z) (at level 70, Y at next level) : stdpp_scope.
(** The class [Lexico A] is used for the lexicographic order on [A]. This order
is used to create finite maps, finite sets, etc, and is typically different from
@@ 790,29 +790,29 @@ Hint Mode Lexico ! : typeclass_instances.
Class ElemOf A B := elem_of: A → B → Prop.
Hint Mode ElemOf  ! : typeclass_instances.
Instance: Params (@elem_of) 3.
Infix "∈" := elem_of (at level 70) : C_scope.
Notation "(∈)" := elem_of (only parsing) : C_scope.
Notation "( x ∈)" := (elem_of x) (only parsing) : C_scope.
Notation "(∈ X )" := (λ x, elem_of x X) (only parsing) : C_scope.
Notation "x ∉ X" := (¬x ∈ X) (at level 80) : C_scope.
Notation "(∉)" := (λ x X, x ∉ X) (only parsing) : C_scope.
Notation "( x ∉)" := (λ X, x ∉ X) (only parsing) : C_scope.
Notation "(∉ X )" := (λ x, x ∉ X) (only parsing) : C_scope.
+Infix "∈" := elem_of (at level 70) : stdpp_scope.
+Notation "(∈)" := elem_of (only parsing) : stdpp_scope.
+Notation "( x ∈)" := (elem_of x) (only parsing) : stdpp_scope.
+Notation "(∈ X )" := (λ x, elem_of x X) (only parsing) : stdpp_scope.
+Notation "x ∉ X" := (¬x ∈ X) (at level 80) : stdpp_scope.
+Notation "(∉)" := (λ x X, x ∉ X) (only parsing) : stdpp_scope.
+Notation "( x ∉)" := (λ X, x ∉ X) (only parsing) : stdpp_scope.
+Notation "(∉ X )" := (λ x, x ∉ X) (only parsing) : stdpp_scope.
Class Disjoint A := disjoint : A → A → Prop.
Hint Mode Disjoint ! : typeclass_instances.
Instance: Params (@disjoint) 2.
Infix "##" := disjoint (at level 70) : C_scope.
Notation "(##)" := disjoint (only parsing) : C_scope.
Notation "( X ##.)" := (disjoint X) (only parsing) : C_scope.
Notation "(.## X )" := (λ Y, Y ## X) (only parsing) : C_scope.
Infix "##*" := (Forall2 (##)) (at level 70) : C_scope.
Notation "(##*)" := (Forall2 (##)) (only parsing) : C_scope.
Infix "##**" := (Forall2 (##*)) (at level 70) : C_scope.
Infix "##1*" := (Forall2 (λ p q, p.1 ## q.1)) (at level 70) : C_scope.
Infix "##2*" := (Forall2 (λ p q, p.2 ## q.2)) (at level 70) : C_scope.
Infix "##1**" := (Forall2 (λ p q, p.1 ##* q.1)) (at level 70) : C_scope.
Infix "##2**" := (Forall2 (λ p q, p.2 ##* q.2)) (at level 70) : C_scope.
+Infix "##" := disjoint (at level 70) : stdpp_scope.
+Notation "(##)" := disjoint (only parsing) : stdpp_scope.
+Notation "( X ##.)" := (disjoint X) (only parsing) : stdpp_scope.
+Notation "(.## X )" := (λ Y, Y ## X) (only parsing) : stdpp_scope.
+Infix "##*" := (Forall2 (##)) (at level 70) : stdpp_scope.
+Notation "(##*)" := (Forall2 (##)) (only parsing) : stdpp_scope.
+Infix "##**" := (Forall2 (##*)) (at level 70) : stdpp_scope.
+Infix "##1*" := (Forall2 (λ p q, p.1 ## q.1)) (at level 70) : stdpp_scope.
+Infix "##2*" := (Forall2 (λ p q, p.2 ## q.2)) (at level 70) : stdpp_scope.
+Infix "##1**" := (Forall2 (λ p q, p.1 ##* q.1)) (at level 70) : stdpp_scope.
+Infix "##2**" := (Forall2 (λ p q, p.2 ##* q.2)) (at level 70) : stdpp_scope.
Hint Extern 0 (_ ## _) => symmetry; eassumption.
Hint Extern 0 (_ ##* _) => symmetry; eassumption.
@@ 820,23 +820,23 @@ Class DisjointE E A := disjointE : E → A → A → Prop.
Hint Mode DisjointE  ! : typeclass_instances.
Instance: Params (@disjointE) 4.
Notation "X ##{ Γ } Y" := (disjointE Γ X Y)
 (at level 70, format "X ##{ Γ } Y") : C_scope.
Notation "(##{ Γ } )" := (disjointE Γ) (only parsing, Γ at level 1) : C_scope.
+ (at level 70, format "X ##{ Γ } Y") : stdpp_scope.
+Notation "(##{ Γ } )" := (disjointE Γ) (only parsing, Γ at level 1) : stdpp_scope.
Notation "Xs ##{ Γ }* Ys" := (Forall2 (##{Γ}) Xs Ys)
 (at level 70, format "Xs ##{ Γ }* Ys") : C_scope.
+ (at level 70, format "Xs ##{ Γ }* Ys") : stdpp_scope.
Notation "(##{ Γ }* )" := (Forall2 (##{Γ}))
 (only parsing, Γ at level 1) : C_scope.
+ (only parsing, Γ at level 1) : stdpp_scope.
Notation "X ##{ Γ1 , Γ2 , .. , Γ3 } Y" := (disjoint (pair .. (Γ1, Γ2) .. Γ3) X Y)
 (at level 70, format "X ##{ Γ1 , Γ2 , .. , Γ3 } Y") : C_scope.
+ (at level 70, format "X ##{ Γ1 , Γ2 , .. , Γ3 } Y") : stdpp_scope.
Notation "Xs ##{ Γ1 , Γ2 , .. , Γ3 }* Ys" :=
(Forall2 (disjoint (pair .. (Γ1, Γ2) .. Γ3)) Xs Ys)
 (at level 70, format "Xs ##{ Γ1 , Γ2 , .. , Γ3 }* Ys") : C_scope.
+ (at level 70, format "Xs ##{ Γ1 , Γ2 , .. , Γ3 }* Ys") : stdpp_scope.
Hint Extern 0 (_ ##{_} _) => symmetry; eassumption.
Class DisjointList A := disjoint_list : list A → Prop.
Hint Mode DisjointList ! : typeclass_instances.
Instance: Params (@disjoint_list) 2.
Notation "## Xs" := (disjoint_list Xs) (at level 20, format "## Xs") : C_scope.
+Notation "## Xs" := (disjoint_list Xs) (at level 20, format "## Xs") : stdpp_scope.
Section disjoint_list.
Context `{Disjoint A, Union A, Empty A}.
@@ 881,32 +881,32 @@ Class OMap (M : Type → Type) := omap: ∀ {A B}, (A → option B) → M A →
Arguments omap {_ _ _ _} _ !_ / : assert.
Instance: Params (@omap) 4.
Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : C_scope.
Notation "( m ≫=)" := (λ f, mbind f m) (only parsing) : C_scope.
Notation "(≫= f )" := (mbind f) (only parsing) : C_scope.
Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : C_scope.
+Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : stdpp_scope.
+Notation "( m ≫=)" := (λ f, mbind f m) (only parsing) : stdpp_scope.
+Notation "(≫= f )" := (mbind f) (only parsing) : stdpp_scope.
+Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : stdpp_scope.
Notation "x ← y ; z" := (y ≫= (λ x : _, z))
 (at level 100, only parsing, right associativity) : C_scope.
+ (at level 100, only parsing, right associativity) : stdpp_scope.
Infix "<$>" := fmap (at level 60, right associativity) : C_scope.
+Infix "<$>" := fmap (at level 60, right associativity) : stdpp_scope.
Notation "' ( x1 , x2 ) ← y ; z" :=
(y ≫= (λ x : _, let ' (x1, x2) := x in z))
 (at level 100, z at level 200, only parsing, right associativity) : C_scope.
+ (at level 100, z at level 200, only parsing, right associativity) : stdpp_scope.
Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
(y ≫= (λ x : _, let ' (x1,x2,x3) := x in z))
 (at level 100, z at level 200, only parsing, right associativity) : C_scope.
+ (at level 100, z at level 200, only parsing, right associativity) : stdpp_scope.
Notation "' ( x1 , x2 , x3 , x4 ) ← y ; z" :=
(y ≫= (λ x : _, let ' (x1,x2,x3,x4) := x in z))
 (at level 100, z at level 200, only parsing, right associativity) : C_scope.
+ (at level 100, z at level 200, only parsing, right associativity) : stdpp_scope.
Notation "' ( x1 , x2 , x3 , x4 , x5 ) ← y ; z" :=
(y ≫= (λ x : _, let ' (x1,x2,x3,x4,x5) := x in z))
 (at level 100, z at level 200, only parsing, right associativity) : C_scope.
+ (at level 100, z at level 200, only parsing, right associativity) : stdpp_scope.
Notation "' ( x1 , x2 , x3 , x4 , x5 , x6 ) ← y ; z" :=
(y ≫= (λ x : _, let ' (x1,x2,x3,x4,x5,x6) := x in z))
 (at level 100, z at level 200, only parsing, right associativity) : C_scope.
+ (at level 100, z at level 200, only parsing, right associativity) : stdpp_scope.
Notation "x ;; z" := (x ≫= λ _, z)
 (at level 100, z at level 200, only parsing, right associativity): C_scope.
+ (at level 100, z at level 200, only parsing, right associativity): stdpp_scope.
Notation "ps .*1" := (fmap (M:=list) fst ps)
(at level 10, format "ps .*1").
@@ 917,9 +917,9 @@ Class MGuard (M : Type → Type) :=
mguard: ∀ P {dec : Decision P} {A}, (P → M A) → M A.
Arguments mguard _ _ _ !_ _ _ / : assert.
Notation "'guard' P ; z" := (mguard P (λ _, z))
 (at level 100, z at level 200, only parsing, right associativity) : C_scope.
+ (at level 100, z at level 200, only parsing, right associativity) : stdpp_scope.
Notation "'guard' P 'as' H ; z" := (mguard P (λ H, z))
 (at level 100, z at level 200, only parsing, right associativity) : C_scope.
+ (at level 100, z at level 200, only parsing, right associativity) : stdpp_scope.
(** * Operations on maps *)
(** In this section we define operational type classes for the operations
@@ 928,17 +928,17 @@ The function look up [m !! k] should yield the element at key [k] in [m]. *)
Class Lookup (K A M : Type) := lookup: K → M → option A.
Hint Mode Lookup   ! : typeclass_instances.
Instance: Params (@lookup) 4.
Notation "m !! i" := (lookup i m) (at level 20) : C_scope.
Notation "(!!)" := lookup (only parsing) : C_scope.
Notation "( m !!)" := (λ i, m !! i) (only parsing) : C_scope.
Notation "(!! i )" := (lookup i) (only parsing) : C_scope.
+Notation "m !! i" := (lookup i m) (at level 20) : stdpp_scope.
+Notation "(!!)" := lookup (only parsing) : stdpp_scope.
+Notation "( m !!)" := (λ i, m !! i) (only parsing) : stdpp_scope.
+Notation "(!! i )" := (lookup i) (only parsing) : stdpp_scope.
Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert.
(** The singleton map *)
Class SingletonM K A M := singletonM: K → A → M.
Hint Mode SingletonM   ! : typeclass_instances.
Instance: Params (@singletonM) 5.
Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : C_scope.
+Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : stdpp_scope.
(** The function insert [<[k:=a]>m] should update the element at key [k] with
value [a] in [m]. *)
@@ 946,7 +946,7 @@ Class Insert (K A M : Type) := insert: K → A → M → M.
Hint Mode Insert   ! : typeclass_instances.
Instance: Params (@insert) 5.
Notation "<[ k := a ]>" := (insert k a)
 (at level 5, right associativity, format "<[ k := a ]>") : C_scope.
+ (at level 5, right associativity, format "<[ k := a ]>") : stdpp_scope.
Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
(** The function delete [delete k m] should delete the value at key [k] in
@@ 1020,15 +1020,15 @@ Class LookupE (E K A M : Type) := lookupE: E → K → M → option A.
Hint Mode LookupE    ! : typeclass_instances.
Instance: Params (@lookupE) 6.
Notation "m !!{ Γ } i" := (lookupE Γ i m)
 (at level 20, format "m !!{ Γ } i") : C_scope.
Notation "(!!{ Γ } )" := (lookupE Γ) (only parsing, Γ at level 1) : C_scope.
+ (at level 20, format "m !!{ Γ } i") : stdpp_scope.
+Notation "(!!{ Γ } )" := (lookupE Γ) (only parsing, Γ at level 1) : stdpp_scope.
Arguments lookupE _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
Class InsertE (E K A M : Type) := insertE: E → K → A → M → M.
Hint Mode InsertE    ! : typeclass_instances.
Instance: Params (@insertE) 6.
Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a)
 (at level 5, right associativity, format "<[ k := a ]{ Γ }>") : C_scope.
+ (at level 5, right associativity, format "<[ k := a ]{ Γ }>") : stdpp_scope.
Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
@@ 1128,5 +1128,5 @@ Class FreshSpec A C `{ElemOf A C,
(** * Miscellaneous *)
Class Half A := half: A → A.
Hint Mode Half ! : typeclass_instances.
Notation "½" := half : C_scope.
Notation "½*" := (fmap (M:=list) half) : C_scope.
+Notation "½" := half : stdpp_scope.
+Notation "½*" := (fmap (M:=list) half) : stdpp_scope.
diff git a/theories/fin_maps.v b/theories/fin_maps.v
index 03e5c5c63c87756941a0f4a0511008ece25574ba..91af5b33e7f8393a4cf58c88e2f6840912fd1b8b 100644
 a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ 92,10 +92,10 @@ Definition map_included `{∀ A, Lookup K A (M A)} {A}
(R : relation A) : relation (M A) := map_relation R (λ _, False) (λ _, True).
Definition map_disjoint `{∀ A, Lookup K A (M A)} {A} : relation (M A) :=
map_relation (λ _ _, False) (λ _, True) (λ _, True).
Infix "##ₘ" := map_disjoint (at level 70) : C_scope.
+Infix "##ₘ" := map_disjoint (at level 70) : stdpp_scope.
Hint Extern 0 (_ ##ₘ _) => symmetry; eassumption.
Notation "( m ##ₘ.)" := (map_disjoint m) (only parsing) : C_scope.
Notation "(.##ₘ m )" := (λ m2, m2 ##ₘ m) (only parsing) : C_scope.
+Notation "( m ##ₘ.)" := (map_disjoint m) (only parsing) : stdpp_scope.
+Notation "(.##ₘ m )" := (λ m2, m2 ##ₘ m) (only parsing) : stdpp_scope.
Instance map_subseteq `{∀ A, Lookup K A (M A)} {A} : SubsetEq (M A) :=
map_included (=).
diff git a/theories/list.v b/theories/list.v
index c2cbd8bc9236b217005a3d6c1b588cd43be4a1f4..532224f0fcbd62eabfb00dea9fd1f6b4412504c6 100644
 a/theories/list.v
+++ b/theories/list.v
@@ 30,21 +30,21 @@ Arguments Permutation {_} _ _ : assert.
Arguments Forall_cons {_} _ _ _ _ _ : assert.
Remove Hints Permutation_cons : typeclass_instances.
Notation "(::)" := cons (only parsing) : C_scope.
Notation "( x ::)" := (cons x) (only parsing) : C_scope.
Notation "(:: l )" := (λ x, cons x l) (only parsing) : C_scope.
Notation "(++)" := app (only parsing) : C_scope.
Notation "( l ++)" := (app l) (only parsing) : C_scope.
Notation "(++ k )" := (λ l, app l k) (only parsing) : C_scope.

Infix "≡ₚ" := Permutation (at level 70, no associativity) : C_scope.
Notation "(≡ₚ)" := Permutation (only parsing) : C_scope.
Notation "( x ≡ₚ)" := (Permutation x) (only parsing) : C_scope.
Notation "(≡ₚ x )" := (λ y, y ≡ₚ x) (only parsing) : C_scope.
Notation "(≢ₚ)" := (λ x y, ¬x ≡ₚ y) (only parsing) : C_scope.
Notation "x ≢ₚ y":= (¬x ≡ₚ y) (at level 70, no associativity) : C_scope.
Notation "( x ≢ₚ)" := (λ y, x ≢ₚ y) (only parsing) : C_scope.
Notation "(≢ₚ x )" := (λ y, y ≢ₚ x) (only parsing) : C_scope.
+Notation "(::)" := cons (only parsing) : stdpp_scope.
+Notation "( x ::)" := (cons x) (only parsing) : stdpp_scope.
+Notation "(:: l )" := (λ x, cons x l) (only parsing) : stdpp_scope.
+Notation "(++)" := app (only parsing) : stdpp_scope.
+Notation "( l ++)" := (app l) (only parsing) : stdpp_scope.
+Notation "(++ k )" := (λ l, app l k) (only parsing) : stdpp_scope.
+
+Infix "≡ₚ" := Permutation (at level 70, no associativity) : stdpp_scope.
+Notation "(≡ₚ)" := Permutation (only parsing) : stdpp_scope.
+Notation "( x ≡ₚ)" := (Permutation x) (only parsing) : stdpp_scope.
+Notation "(≡ₚ x )" := (λ y, y ≡ₚ x) (only parsing) : stdpp_scope.
+Notation "(≢ₚ)" := (λ x y, ¬x ≡ₚ y) (only parsing) : stdpp_scope.
+Notation "x ≢ₚ y":= (¬x ≡ₚ y) (at level 70, no associativity) : stdpp_scope.
+Notation "( x ≢ₚ)" := (λ y, x ≢ₚ y) (only parsing) : stdpp_scope.
+Notation "(≢ₚ x )" := (λ y, y ≢ₚ x) (only parsing) : stdpp_scope.
Instance maybe_cons {A} : Maybe2 (@cons A) := λ l,
match l with x :: l => Some (x,l)  _ => None end.
@@ 240,8 +240,8 @@ Fixpoint permutations {A} (l : list A) : list (list A) :=
The predicate [prefix] holds if the first list is a prefix of the second. *)
Definition suffix {A} : relation (list A) := λ l1 l2, ∃ k, l2 = k ++ l1.
Definition prefix {A} : relation (list A) := λ l1 l2, ∃ k, l2 = l1 ++ k.
Infix "`suffix_of`" := suffix (at level 70) : C_scope.
Infix "`prefix_of`" := prefix (at level 70) : C_scope.
+Infix "`suffix_of`" := suffix (at level 70) : stdpp_scope.
+Infix "`prefix_of`" := prefix (at level 70) : stdpp_scope.
Hint Extern 0 (_ `prefix_of` _) => reflexivity.
Hint Extern 0 (_ `suffix_of` _) => reflexivity.
@@ 271,7 +271,7 @@ Inductive sublist {A} : relation (list A) :=
 sublist_nil : sublist [] []
 sublist_skip x l1 l2 : sublist l1 l2 → sublist (x :: l1) (x :: l2)
 sublist_cons x l1 l2 : sublist l1 l2 → sublist l1 (x :: l2).
Infix "`sublist_of`" := sublist (at level 70) : C_scope.
+Infix "`sublist_of`" := sublist (at level 70) : stdpp_scope.
Hint Extern 0 (_ `sublist_of` _) => reflexivity.
(** A list [l2] submseteq a list [l1] if [l2] is obtained by removing elements
@@ 282,7 +282,7 @@ Inductive submseteq {A} : relation (list A) :=
 submseteq_swap x y l : submseteq (y :: x :: l) (x :: y :: l)
 submseteq_cons x l1 l2 : submseteq l1 l2 → submseteq l1 (x :: l2)
 submseteq_trans l1 l2 l3 : submseteq l1 l2 → submseteq l2 l3 → submseteq l1 l3.
Infix "⊆+" := submseteq (at level 70) : C_scope.
+Infix "⊆+" := submseteq (at level 70) : stdpp_scope.
Hint Extern 0 (_ ⊆+ _) => reflexivity.
(** Removes [x] from the list [l]. The function returns a [Some] when the
diff git a/theories/set.v b/theories/set.v
index 9da4261094bb5cfa4d82e6bb0e0ca3f1a711a029..39e389aed41a86f59a3a845d08440e3cd895736b 100644
 a/theories/set.v
+++ b/theories/set.v
@@ 9,7 +9,7 @@ Add Printing Constructor set.
Arguments mkSet {_} _ : assert.
Arguments set_car {_} _ _ : assert.
Notation "{[ x  P ]}" := (mkSet (λ x, P))
 (at level 1, format "{[ x  P ]}") : C_scope.
+ (at level 1, format "{[ x  P ]}") : stdpp_scope.
Instance set_elem_of {A} : ElemOf A (set A) := λ x X, set_car X x.
diff git a/theories/strings.v b/theories/strings.v
index b028d4942ad855a156675ac79deb5df1f08e3932..d7ba9adb9b097b1cc57cbf0730af710fa8d6ff26 100644
 a/theories/strings.v
+++ b/theories/strings.v
@@ 13,7 +13,7 @@ Notation length := List.length.
(** * Fix scopes *)
Open Scope string_scope.
Open Scope list_scope.
Infix "+:+" := String.append (at level 60, right associativity) : C_scope.
+Infix "+:+" := String.append (at level 60, right associativity) : stdpp_scope.
Arguments String.append : simpl never.
(** * Decision of equality *)