From 4ec8646c1bf426c848e8057cdf7c248df6999523 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 9 Nov 2022 22:03:04 +0100
Subject: Make a minor cleanup

---
 compiler/ExtractToFStar.ml | 11 +----------
 1 file changed, 1 insertion(+), 10 deletions(-)

(limited to 'compiler/ExtractToFStar.ml')

diff --git a/compiler/ExtractToFStar.ml b/compiler/ExtractToFStar.ml
index a995d4a6..fc04ce90 100644
--- a/compiler/ExtractToFStar.ml
+++ b/compiler/ExtractToFStar.ml
@@ -1456,16 +1456,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
        *)
       let inputs_lvs =
         let all_inputs = (Option.get def.body).inputs_lvs in
-        (* We have to count:
-         * - the forward inputs
-         * - the state (if there is one)
-         *)
-        let num_fwd_inputs = def.signature.info.num_fwd_inputs in
-        let num_fwd_inputs =
-          if def.signature.info.effect_info.stateful_group then
-            1 + num_fwd_inputs
-          else num_fwd_inputs
-        in
+        let num_fwd_inputs = def.signature.info.num_fwd_inputs_with_state in
         Collections.List.prefix num_fwd_inputs all_inputs
       in
       let _ =
-- 
cgit v1.2.3