3 files changed, 3 insertions, 4 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index d1eabcab..9cd0b31b 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -221,7 +221,7 @@ Definition all (A:Type) (P:A -> Prop) := forall x:A, P x.
 
 Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..))
   (at level 200, x binder, right associativity,
-   format "'[' 'exists'  '/  ' x .. y ,  '/  ' p ']'")
+   format "'[' 'exists'  '/  ' x  ..  y ,  '/  ' p ']'")
   : type_scope.
 
 Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q))
@@ -404,7 +404,7 @@ Definition uniqueness (A:Type) (P:A->Prop) := forall x y, P x -> P y -> x = y.
 Notation "'exists' ! x .. y , p" :=
   (ex (unique (fun x => .. (ex (unique (fun y => p))) ..)))
   (at level 200, x binder, right associativity,
-   format "'[' 'exists'  !  '/  ' x .. y ,  '/  ' p ']'")
+   format "'[' 'exists'  !  '/  ' x  ..  y ,  '/  ' p ']'")
   : type_scope.
 
 Lemma unique_existence : forall (A:Type) (P:A->Prop),
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index e929c561..d85f5363 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -19,7 +19,6 @@ Declare ML Module "extraction_plugin".
 Declare ML Module "decl_mode_plugin".
 Declare ML Module "cc_plugin".
 Declare ML Module "ground_plugin".
-Declare ML Module "dp_plugin".
 Declare ML Module "recdef_plugin".
 Declare ML Module "subtac_plugin".
 Declare ML Module "xml_plugin".
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 637994b2..5b7afc99 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -60,7 +60,7 @@ Add Printing Let sigT2.
 
 (** Projections of [sig]
 
-    An element [y] of a subset [{x:A & (P x)}] is the pair of an [a]
+    An element [y] of a subset [{x:A | (P x)}] is the pair of an [a]
     of type [A] and of a proof [h] that [a] satisfies [P].  Then
     [(proj1_sig y)] is the witness [a] and [(proj2_sig y)] is the
     proof of [(P a)] *)