Verified Commit b36cd736 authored by Tej Chajed's avatar Tej Chajed

Remove type scope from forall notation

Fixes #67.
parent 60ad150d
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment