notation for forall

theories/base.v

@@ -182,12 +182,12 @@ Delimit Scope stdpp_scope with stdpp.
 Global Open Scope stdpp_scope.
 
 (** Change [True], [False], and [forall] into notations in order to enable overloading.
-We will use this to give [True] and [False] a different interpretation for
+We will use this to give them a different interpretation for
 embedded logics. *)
 Notation "'True'" := True (format "True") : type_scope.
 Notation "'False'" := False (format "False") : type_scope.
 Notation "'forall' x .. y , P" :=
-  (forall x, .. (forall y, P%type) ..) (at level 200, x binder, y binder, right associativity) : type_scope.
+  (forall x, .. (forall y, P) ..) (at level 200, x binder, y binder, right associativity, only parsing) : type_scope.
 
 
 (** * Equality *)