From e161eb47d51a01e54a21c4517c85ef4c5525709e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 9 Feb 2022 13:00:47 +0100
Subject: Add more command line arguments for the decrease clauses

---
 src/Translate.ml | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'src/Translate.ml')

diff --git a/src/Translate.ml b/src/Translate.ml
index aa73ab7c..da0b32a4 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -24,6 +24,16 @@ type config = {
           let _ = assert_norm (FUNCTION () = Success ())
           ```
        *)
+  extract_decrease_clauses : bool;
+      (** If true, insert `decrease` clauses for all the recursive definitions.
+
+          The body of such clauses must be defined by the user.
+       *)
+  extract_template_decrease_clauses : bool;
+      (** In order to help the user, we can generate "template" decrease clauses
+          (i.e., definitions with proper signatures but dummy bodies) in a
+          dedicated file.
+       *)
 }
 
 type symbolic_fun_translation = V.symbolic_value list * SA.expression
-- 
cgit v1.2.3