aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/Renaming.v
diff options
context:
space:
mode:
authorMichalis Pardalos <m.pardalos@gmail.com>2021-08-30 22:15:02 +0100
committerMichalis Pardalos <m.pardalos@gmail.com>2021-08-30 22:15:02 +0100
commit8bc6214e053aa4487abfbd895c00e2da9f21bd8a (patch)
tree2301479ca921c014a57ca419fbeb32f17624e7e7 /src/hls/Renaming.v
parentb067e5c7b0ecce9ffbf21e9c4a7ff96328dec2ba (diff)
downloadvericert-8bc6214e053aa4487abfbd895c00e2da9f21bd8a.tar.gz
vericert-8bc6214e053aa4487abfbd895c00e2da9f21bd8a.zip
WIP
Diffstat (limited to 'src/hls/Renaming.v')
-rw-r--r--src/hls/Renaming.v8
1 files changed, 4 insertions, 4 deletions
diff --git a/src/hls/Renaming.v b/src/hls/Renaming.v
index b9fbcaa..6c816c2 100644
--- a/src/hls/Renaming.v
+++ b/src/hls/Renaming.v
@@ -102,12 +102,12 @@ Fixpoint renumber_stmnt (stmnt : Verilog.stmnt) :=
ret (Vcond e' s1' s2')
| Vcase e cs def =>
do e' <- renumber_expr e;
- do cs' <- sequence (map
- (fun (c : (Verilog.expr * Verilog.stmnt)) =>
- let (c_expr, c_stmnt) := c in
+ do cs_list' <- sequence (map
+ (fun '(c_expr, c_stmnt) =>
do expr' <- renumber_expr c_expr;
do stmnt' <- renumber_stmnt c_stmnt;
- ret (expr', stmnt')) cs);
+ ret (expr', stmnt')) (stmnt_to_list cs));
+ let cs' := list_to_stmnt cs_list' in
do def' <- match def with
| None => ret None
| Some d => do def' <- renumber_stmnt d; ret (Some def')