diff options
Diffstat (limited to 'src/Translate.ml')
| -rw-r--r-- | src/Translate.ml | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/src/Translate.ml b/src/Translate.ml index a264a121..d5505894 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -481,19 +481,13 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) let has_decr_clause = has_decreases_clause def && config.extract_decreases_clauses in - (* Is there an input parameter "visible" for the state used in - * the state error monad (if we use a state error monad)? *) - let has_state_param = - config.use_state_monad - && config.mp_config.unfold_monadic_let_bindings - in (* Check if the definition needs to be filtered or not *) if ((not is_opaque) && config.extract_transparent) || (is_opaque && config.extract_opaque) then ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif - has_decr_clause has_state_param fwd_def def) + has_decr_clause def) fls); (* Insert unit tests if necessary *) if config.test_unit_functions then |