diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Translate.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml index b2cab4c2..139f8891 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -825,12 +825,14 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : let ctx = List.fold_left (fun ctx (keep_fwd, defs) -> - (* We generate a decrease clause for all the recursive functions *) + (* If requested by the user, register termination measures and decreases + proofs for all the recursive functions *) let fwd_def = fst (fst defs) in let gen_decr_clause (def : Pure.fun_decl) = - PureUtils.FunLoopIdSet.mem - (def.Pure.def_id, def.Pure.loop_id) - rec_functions + !Config.extract_decreases_clauses + && PureUtils.FunLoopIdSet.mem + (def.Pure.def_id, def.Pure.loop_id) + rec_functions in (* Register the names, only if the function is not a global body - * those are handled later *) |