From 01431eb67ed566baa2268f1382d687bc7b020d1c Mon Sep 17 00:00:00 2001
From: vblot <24938579+vblot@users.noreply.github.com>
Date: Wed, 25 Aug 2021 14:56:41 +0200
Subject: fix array notations clash with ssreflect

---
 src/versions/standard/Array/PArray_standard.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src/versions')

diff --git a/src/versions/standard/Array/PArray_standard.v b/src/versions/standard/Array/PArray_standard.v
index f3bf606..947eb49 100644
--- a/src/versions/standard/Array/PArray_standard.v
+++ b/src/versions/standard/Array/PArray_standard.v
@@ -69,9 +69,11 @@ Definition map {A B:Type} (f:A -> B) (t:array A) : array B :=
   let (t,d) := td in
   (Map.map f t, f d, l).
 
+Module Export PArrayNotations.
 Delimit Scope array_scope with array.
 Notation "t '.[' i ']'" := (get t i) (at level 50) : array_scope.
 Notation "t '.[' i '<-' a ']'" := (set t i a) (at level 50) : array_scope.
+End PArrayNotations.
 
 Local Open Scope array_scope.
 
-- 
cgit