diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-09-24 12:57:32 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-09-24 12:57:32 +0100 |
commit | 244270b446721d5eeb1ed15ec2839aa4d246965c (patch) | |
tree | de81d86a1d919d7537cfa210f854cd81a8142777 /src/hls/RTLPargen.v | |
parent | d8609f77bf5a29c52da8f51b3a248050716c30a4 (diff) | |
download | vericert-244270b446721d5eeb1ed15ec2839aa4d246965c.tar.gz vericert-244270b446721d5eeb1ed15ec2839aa4d246965c.zip |
Fix scoping
Diffstat (limited to 'src/hls/RTLPargen.v')
-rw-r--r-- | src/hls/RTLPargen.v | 22 |
1 files 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). |