diff options
author | Son Ho | 2022-02-09 18:32:18 +0100 |
---|---|---|
committer | Son Ho | 2022-02-09 18:32:18 +0100 |
commit | 1f6798412509e0020f3ad468bfe91d3b15a7ce75 (patch) | |
tree | 01083cda8fd141bc4355de736353203986c3fb54 /src/main.ml | |
parent | b6b77b38a16a102d3ccbc8bfad5a81a04eb3643d (diff) |
Cleanup a bit
Diffstat (limited to '')
-rw-r--r-- | src/main.ml | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/main.ml b/src/main.ml index fdd0576e..7bec093d 100644 --- a/src/main.ml +++ b/src/main.ml @@ -30,8 +30,8 @@ let () = let filter_useless_functions = ref true in let test_units = ref false in let test_trans_units = ref false in - let no_decrease_clauses = ref false in - let template_decrease_clauses = ref false in + let no_decreases_clauses = ref false in + let template_decreases_clauses = ref false in let no_split = ref false in let spec = @@ -64,15 +64,15 @@ let () = Arg.Set test_trans_units, " Test the translated unit functions with the target theorem\n\ \ prover's normalizer" ); - ( "-no-decrease-clauses", - Arg.Set no_decrease_clauses, + ( "-no-decreases-clauses", + Arg.Set no_decreases_clauses, " Do not add decrease clauses to the recursive definitions" ); ( "-template-clauses", - Arg.Set template_decrease_clauses, - " Generate templates for the required decrease clauses, in a\n\ + Arg.Set template_decreases_clauses, + " Generate templates for the required decreases clauses, in a\n\ `\n\ \ dedicated file. Incompatible with \ - -no-decrease-clauses" ); + -no-decreases-clauses" ); ( "-no-split", Arg.Set no_split, " Don't split the definitions between different files for types, \ @@ -80,7 +80,7 @@ let () = ] in (* Sanity check: -template-clauses ==> not -no-decrease-clauses *) - assert ((not !no_decrease_clauses) || not !template_decrease_clauses); + assert ((not !no_decreases_clauses) || not !template_decreases_clauses); let spec = Arg.align spec in let filenames = ref [] in @@ -176,8 +176,8 @@ let () = mp_config = micro_passes_config; split_files = not !no_split; test_unit_functions; - extract_decrease_clauses = not !no_decrease_clauses; - extract_template_decrease_clauses = !template_decrease_clauses; + extract_decreases_clauses = not !no_decreases_clauses; + extract_template_decreases_clauses = !template_decreases_clauses; } in Translate.translate_module filename dest_dir trans_config m |