diff options
Diffstat (limited to 'compiler/Translate.ml')
| -rw-r--r-- | compiler/Translate.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 4ca9eff2..0a1c8f9a 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -563,7 +563,10 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) let extract_decrease decl = let has_decr_clause = has_decreases_clause decl in if has_decr_clause then - Extract.extract_template_decreases_clause ctx.extract_ctx fmt decl + if !Config.backend = Lean then + Extract.extract_termination_and_decreasing ctx.extract_ctx fmt decl + else + Extract.extract_template_decreases_clause ctx.extract_ctx fmt decl in extract_decrease fwd; List.iter extract_decrease loop_fwds) |