summaryrefslogtreecommitdiff
path: root/compiler/Config.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Config.ml9
1 files changed, 6 insertions, 3 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml
index 584635bc..98a5eea1 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -214,10 +214,13 @@ let test_trans_unit_functions = ref false
let extract_decreases_clauses = ref false
(** In order to help the user, we can generate "template" decrease clauses/ termination
- measures (i.e., definitions with proper signatures but dummy bodies) in a dedicated
- file.
+ measures (i.e., definitions with proper signatures but dummy bodies) in a dedicated
+ file.
+
+ We initialize it to [true], then deactivate it depending on the CL options
+ given by the user.
*)
-let extract_template_decreases_clauses = ref false
+let extract_template_decreases_clauses = ref true
(** {1 Micro passes} *)