From 5c069266f5f2fa9212575d036385aeaec7622069 Mon Sep 17 00:00:00 2001
From: David Swasey <swasey@mpi-sws.org>
Date: Wed, 29 Nov 2017 15:19:45 +0100
Subject: [PATCH] Make x.1, x.2 notation compatible with ssrfun.

Enable one to import both stdpp's base and ssrfun.

Note that (f x.1) now parses as (f (fst x)) rather than (fst (f x)).
(This change affects one proof in Iris.)
---
 theories/base.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 1295da6a..62f9f8f3 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -513,8 +513,8 @@ Instance unit_inhabited: Inhabited unit := populate ().
 Notation "( x ,)" := (pair x) (only parsing) : stdpp_scope.
 Notation "(, y )" := (λ x, (x,y)) (only parsing) : stdpp_scope.
 
-Notation "p .1" := (fst p) (at level 10, format "p .1").
-Notation "p .2" := (snd p) (at level 10, format "p .2").
+Notation "p .1" := (fst p) (at level 2, left associativity, format "p .1").
+Notation "p .2" := (snd p) (at level 2, left associativity, format "p .2").
 
 Instance: Params (@pair) 2.
 Instance: Params (@fst) 2.
@@ -899,9 +899,9 @@ Notation "x ;; z" := (x ≫= λ _, z)
   (at level 100, z at level 200, only parsing, right associativity): stdpp_scope.
 
 Notation "ps .*1" := (fmap (M:=list) fst ps)
-  (at level 10, format "ps .*1").
+  (at level 2, left associativity, format "ps .*1").
 Notation "ps .*2" := (fmap (M:=list) snd ps)
-  (at level 10, format "ps .*2").
+  (at level 2, left associativity, format "ps .*2").
 
 Class MGuard (M : Type → Type) :=
   mguard: ∀ P {dec : Decision P} {A}, (P → M A) → M A.
-- 
GitLab