Adapt to https://github.com/coq/coq/pull/18224

stdpp/base.v

@@ -12,6 +12,10 @@ From Coq Require Export Morphisms RelationClasses List Bool Setoid Peano Utf8.
 From Coq Require Import Permutation.
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
+
+(* notations _.1 and _.2 below, TODO: remove when requiring Coq > 8.19 *)
+From Coq.ssr Require Import (notations) ssrfun.
+
 From stdpp Require Import options.
 
 (** This notation is necessary to prevent [length] from being printed
@@ -722,8 +726,8 @@ Proof. intros [] []; reflexivity. Qed.
 Notation "( x ,.)" := (pair x) (only parsing) : stdpp_scope.
 Notation "(., y )" := (λ x, (x,y)) (only parsing) : stdpp_scope.
 
-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").
+Notation "p .1" := (fst p).
+Notation "p .2" := (snd p).
 
 Global Instance: Params (@pair) 2 := {}.
 Global Instance: Params (@fst) 2 := {}.