aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorMichalis Pardalos <m.pardalos@gmail.com>2021-09-01 14:06:07 +0100
committerMichalis Pardalos <m.pardalos@gmail.com>2021-09-01 14:06:07 +0100
commitadabec157b807bf6695bdcef64233c76f43c37bb (patch)
tree26249a0856dc08226f72df741498d3a768581b95
parent621dcfad451379fdcfad5f84c1d72f73023160f4 (diff)
downloadvericert-adabec157b807bf6695bdcef64233c76f43c37bb.tar.gz
vericert-adabec157b807bf6695bdcef64233c76f43c37bb.zip
Start renaming from 2, fixes wf_params check
-rw-r--r--src/hls/Renaming.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/Renaming.v b/src/hls/Renaming.v
index 714c99b..b088926 100644
--- a/src/hls/Renaming.v
+++ b/src/hls/Renaming.v
@@ -233,7 +233,7 @@ End TRANSF_PROGRAM_STATEFUL.
Definition transf_program (p : HTL.program) : Errors.res HTL.program :=
transform_stateful_program _ _ _
(fun _ f => renumber_fundef f)
- (mk_renumber_state 1%positive (PTree.empty reg))
+ (mk_renumber_state 2%positive (PTree.empty reg))
p.
Definition match_prog : HTL.program -> HTL.program -> Prop := fun _ _ => True.