Skip to content
Snippets Groups Projects

Remove type scope from forall notation

Merged Remove type scope from forall notation
tchajed/stdpp:fix-forall-scope into master
Merged Tej Chajed requested to merge tchajed/stdpp:fix-forall-scope into master
Compare
and
1 file
+ 1
− 1
Compare changes
  • Side-by-side
  • Inline
theories/base.v
+ 1
− 1
@@ -191,7 +191,7 @@ 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) ..)
Notation "'forall' x .. y , P" := (forall x, .. (forall y, P) ..)
(at level 200, x binder, y binder, right associativity,
only parsing) : type_scope.