From 32c8182a6752d29f561e2e742aadc09f05516890 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Fri, 27 Apr 2018 19:47:02 +0200
Subject: [PATCH] Some forgotten occurences of only parsing.
---
theories/base.v | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/theories/base.v b/theories/base.v
index b229cba..9057e4a 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -163,7 +163,8 @@ Infix "=@{ A }" := (@eq A)
(at level 70, only parsing, no associativity) : stdpp_scope.
Notation "(=@{ A } )" := (@eq A) (only parsing) : stdpp_scope.
Notation "(≠@{ A } )" := (λ X Y, ¬X =@{A} Y) (only parsing) : stdpp_scope.
-Notation "X ≠@{ A } Y":= (¬X =@{ A } Y) (at level 70, no associativity) : stdpp_scope.
+Notation "X ≠@{ A } Y":= (¬X =@{ A } Y)
+ (at level 70, only parsing, no associativity) : stdpp_scope.
Hint Extern 0 (_ = _) => reflexivity.
Hint Extern 100 (_ ≠ _) => discriminate.
@@ -193,7 +194,8 @@ Notation "(≢ X )" := (λ Y, Y ≢ X) (only parsing) : stdpp_scope.
Notation "(≡@{ A } )" := (@equiv A _) (only parsing) : stdpp_scope.
Notation "(≢@{ A } )" := (λ X Y, ¬X ≡@{A} Y) (only parsing) : stdpp_scope.
-Notation "X ≢@{ A } Y":= (¬X ≡@{ A } Y) (at level 70, no associativity) : stdpp_scope.
+Notation "X ≢@{ A } Y":= (¬X ≡@{ A } Y)
+ (at level 70, only parsing, no associativity) : stdpp_scope.
(** The type class [LeibnizEquiv] collects setoid equalities that coincide
with Leibniz equality. We provide the tactic [fold_leibniz] to transform such
--
2.26.2