7 files changed, 11 insertions, 13 deletions
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index aa65eb44c8..8555886023 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -21,7 +21,7 @@ Set Implicit Arguments.
 Require Export Classical.
 Require Import ChoiceFacts.
 
-Notation Local "'inhabited' A" := A (at level 200, only parsing).
+Notation Local inhabited A := A.
 
 Axiom constructive_definite_description :
   forall (A : Type) (P : A->Prop), (exists! x : A, P x) -> { x : A | P x }.
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index f3f177a734..6673fa8c96 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -119,7 +119,7 @@ Qed.
 
 *)
 
-Definition inhabited (A:Prop) := A.
+Notation Local inhabited A := A.
 
 Lemma prop_ext_A_eq_A_imp_A :
   prop_extensionality -> forall A:Prop, inhabited A -> (A -> A) = A.
@@ -514,8 +514,6 @@ Qed.
     344 of Lecture Notes in Mathematics, Springer-Verlag, 1973.
 *)
 
-Notation Local "'inhabited' A" := A (at level 10, only parsing).
-
 Definition IndependenceOfGeneralPremises :=
   forall (A:Type) (P:A -> Prop) (Q:Prop),
     inhabited A -> (Q -> exists x, P x) -> exists x, Q -> P x.
diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v
index fe571779ca..83d5e002aa 100644
--- a/theories/Logic/ConstructiveEpsilon.v
+++ b/theories/Logic/ConstructiveEpsilon.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id:$ i*)
+(*i $Id$ i*)
 
 (** This module proves the constructive description schema, which
 infers the sigma-existence (i.e., [Set]-existence) of a witness to a
@@ -53,7 +53,7 @@ of our searching algorithm. *)
 
 Let R (x y : nat) : Prop := x = S y /\ ~ P y.
 
-Notation Local "'acc' x" := (Acc R x) (at level 10).
+Notation Local acc x := (Acc R x).
 
 Lemma P_implies_acc : forall x : nat, P x -> acc x.
 Proof.
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index a954cbef7d..b96ae30e4e 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -267,7 +267,7 @@ End ProofIrrel_RelChoice_imp_EqEM.
 
 (** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *)
 
-Notation Local "'inhabited' A" := A (at level 10, only parsing).
+Notation Local inhabited A := A.
 
 Section ExtensionalEpsilon_imp_EM.
 
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index 92ada3d748..125fd3f127 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -89,8 +89,8 @@ Open Local Scope IntScope.
 Notation "x == y"  := (NZeq x y) (at level 70) : IntScope.
 Notation "x ~= y" := (~ NZeq x y) (at level 70) : IntScope.
 Notation "0" := NZ0 : IntScope.
-Notation "'S'" := NZsucc : IntScope.
-Notation "'P'" := NZpred : IntScope.
+Notation S x := (NZsucc x).
+Notation P x := (NZpred x).
 (*Notation "1" := (S 0) : IntScope.*)
 Notation "x + y" := (NZadd x y) : IntScope.
 Notation "x - y" := (NZsub x y) : IntScope.
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index c4a20506c7..149901c7bb 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -42,8 +42,8 @@ Notation dec := sumbool_of_bool.
 
 (** Hide proofs and generates obligations when put in a term. *)
 
-Notation "'in_left'" := (@left _ _ _) : program_scope.
-Notation "'in_right'" := (@right _ _ _) : program_scope.
+Notation in_left := (@left _ _ _).
+Notation in_right := (@right _ _ _).
 
 (** Extraction directives *)
 (*
@@ -53,4 +53,4 @@ Extract Inductive bool => "bool" [ "true" "false" ].
 Extract Inductive sumbool => "bool" [ "true" "false" ].
 (* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *)
 (* Extract Inductive sigT => "prod" [ "" ]. *)
-*)
-\ No newline at end of file
+*)
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 9ebfa19cb4..f4b57d5bed 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -31,7 +31,7 @@ Notation "a # b" := (Qmake a b) (at level 55, no associativity) : Q_scope.
 Definition inject_Z (x : Z) := Qmake x 1.
 Arguments Scope inject_Z [Z_scope].
 
-Notation " 'QDen'  p " := (Zpos (Qden p)) (at level 20, no associativity) : Q_scope.
+Notation QDen p := (Zpos (Qden p)).
 Notation " 0 " := (0#1) : Q_scope.
 Notation " 1 " := (1#1) : Q_scope.