From 6916990f312abb186a6607f717d020de1fd02a81 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Sun, 10 Jun 2018 15:10:26 +0200
Subject: [PATCH] add format specifier tp single-symbol notation
Works around Coq bug #7731
---
theories/base.v | 12 ++++++------
1 file changed, 6 insertions(+), 6 deletions(-)
diff --git a/theories/base.v b/theories/base.v
index 9057e4a..7967f45 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -146,8 +146,8 @@ Global Open Scope stdpp_scope.
(** 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 : type_scope.
-Notation "'False'" := False : type_scope.
+Notation "'True'" := True (format "True") : type_scope.
+Notation "'False'" := False (format "False") : type_scope.
(** * Equality *)
@@ -747,7 +747,7 @@ intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
[(⊆)] and element of [(∈)] relation, and disjointess [(##)]. *)
Class Empty A := empty: A.
Hint Mode Empty ! : typeclass_instances.
-Notation "∅" := empty : stdpp_scope.
+Notation "∅" := empty (format "∅") : stdpp_scope.
Instance empty_inhabited `(Empty A) : Inhabited A := populate ∅.
@@ -1193,7 +1193,7 @@ Class FreshSpec A C `{ElemOf A C,
(** * Miscellaneous *)
Class Half A := half: A → A.
Hint Mode Half ! : typeclass_instances.
-Notation "½" := half : stdpp_scope.
+Notation "½" := half (format "½") : stdpp_scope.
Notation "½*" := (fmap (M:=list) half) : stdpp_scope.
(** * Notations for lattices. *)
@@ -1232,8 +1232,8 @@ Notation "(⊔ y )" := (λ x, join x y) (only parsing) : stdpp_scope.
Class Top A := top : A.
Hint Mode Top ! : typeclass_instances.
-Notation "⊤" := top : stdpp_scope.
+Notation "⊤" := top (format "⊤") : stdpp_scope.
Class Bottom A := bottom : A.
Hint Mode Bottom ! : typeclass_instances.
-Notation "⊥" := bottom : stdpp_scope.
+Notation "⊥" := bottom (format "⊥") : stdpp_scope.
--
GitLab