summaryrefslogtreecommitdiff
path: root/src/Translate.ml
diff options
context:
space:
mode:
authorSon Ho2022-02-23 23:36:53 +0100
committerSon Ho2022-02-23 23:36:53 +0100
commit532b43ad73a4964cd75d8548d43eb894b7f225c1 (patch)
tree485fc8c35aebd2467878dc18e3f675a9e43175a1 /src/Translate.ml
parente3430dcb5e944af0903b272669e6ddbb8e7d59c3 (diff)
Start working on generating code which uses a state-error monad
Diffstat (limited to 'src/Translate.ml')
-rw-r--r--src/Translate.ml6
1 files changed, 0 insertions, 6 deletions
diff --git a/src/Translate.ml b/src/Translate.ml
index ac2ee38c..077cc32d 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -29,12 +29,6 @@ type config = {
let _ = assert_norm (FUNCTION () = Success ())
```
*)
- use_state_monad : bool;
- (** If `true`, use a state-error monad.
- If `false`, only use an error monad.
-
- Using a state-error monad is necessary when modelling I/O, for instance.
- *)
extract_decreases_clauses : bool;
(** If `true`, insert `decreases` clauses for all the recursive definitions.