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/SMTCoq.v                                  | 2 +-
 src/versions/standard/Array/PArray_standard.v | 2 ++
 2 files changed, 3 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/SMTCoq.v b/src/SMTCoq.v
index 9c85d72..694f2ed 100644
--- a/src/SMTCoq.v
+++ b/src/SMTCoq.v
@@ -11,7 +11,7 @@
 
 
 Require Export PropToBool.
-Require Export Int63 List PArray.
+Require Export Int63 List.
 Require Export SMTCoq.State SMTCoq.SMT_terms SMTCoq.Trace SMT_classes_instances.
 Require Export Tactics.
 Require Export Conversion_tactics.
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