notation for forall

theories/base.v

@@ -186,4+186,4 @@
 
 (** Change [True] and [False] into notations in order to enable overloading.
 We will use this to give [True] and [False] a different interpretation for
 embedded logics. *)
 Notation "'True'" := True (format "True") : type_scope.
 Notation "'False'" := False (format "False") : type_scope.
 
+(** Change [forall] into a notation in order to enable overloading. *)
+Notation "'forall' x .. y , P" := (forall x, .. (forall y, P%type) ..)
+  (at level 200, x binder, y binder, right associativity,
+   only parsing) : type_scope.
+
 
 (** * Equality *)
 (** Introduce some Haskell style like notations. *)