From b36cd73686c95a9e798118e670b6f019d25a81fa Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Wed, 27 May 2020 16:58:10 -0500
Subject: [PATCH] Remove type scope from forall notation
Fixes #67.
---
theories/base.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/base.v b/theories/base.v
index ba67b79b..441535f8 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -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.
--
GitLab