From 244270b446721d5eeb1ed15ec2839aa4d246965c Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 24 Sep 2021 12:57:32 +0100
Subject: Fix scoping

---
 src/hls/RTLPargen.v | 22 ++++++++++------------
 1 file changed, 10 insertions(+), 12 deletions(-)

diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index 208a966..adcd2b3 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -238,11 +238,15 @@ Inductive non_empty (A: Type) :=
 Arguments singleton [A].
 Arguments cons [A].
 
-Delimit Scope list_scope with list.
+Declare Scope non_empty_scope.
+Delimit Scope non_empty_scope with non_empty.
 
-Infix "::|" := cons (at level 60, right associativity) : list_scope.
+Module NonEmptyNotation.
+Infix "::|" := cons (at level 60, right associativity) : non_empty_scope.
+End NonEmptyNotation.
+Import NonEmptyNotation.
 
-#[local] Open Scope list_scope.
+#[local] Open Scope non_empty_scope.
 
 Fixpoint map {A B} (f: A -> B) (l: non_empty A): non_empty B :=
   match l with
@@ -279,17 +283,11 @@ Fixpoint of_list {A} (l: list A): option (non_empty A) :=
   end.
 
 End NonEmpty.
-Module NE := NonEmpty.
-
-Module NonEmptyNotation.
 
-  Notation "A '::|' B" := (NE.cons A B) (at level 70, right associativity) : non_empty.
-
-End NonEmptyNotation.
-Import NonEmptyNotation.
+Module NE := NonEmpty.
+Import NE.NonEmptyNotation.
 
-#[local]
- Open Scope non_empty.
+#[local] Open Scope non_empty_scope.
 
 Definition predicated A := NE.non_empty (option pred_op * A).
 
-- 
cgit