Skip to content
Snippets Groups Projects
Commit 3196e5ca authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'fix-forall-scope' into 'master'

Remove type scope from forall notation

Closes #67

See merge request iris/stdpp!163
parents 60ad150d b36cd736
No related branches found
No related tags found
1 merge request!163Remove type scope from forall notation
Pipeline #28740 passed
...@@ -191,7 +191,7 @@ Notation "'True'" := True (format "True") : type_scope. ...@@ -191,7 +191,7 @@ Notation "'True'" := True (format "True") : type_scope.
Notation "'False'" := False (format "False") : type_scope. Notation "'False'" := False (format "False") : type_scope.
(** Change [forall] into a notation in order to enable overloading. *) (** 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, (at level 200, x binder, y binder, right associativity,
only parsing) : type_scope. only parsing) : type_scope.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment