From 1d33206096d019d4593fd11e4257b0d786666d87 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 7 Mar 2023 09:42:43 +0100
Subject: Consistently use the names TerminationMeasure and DecreasesProof

---
 compiler/Translate.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'compiler/Translate.ml')

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 *)
-- 
cgit v1.2.3