summaryrefslogtreecommitdiff
path: root/compiler/Pure.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Pure.ml12
1 files changed, 1 insertions, 11 deletions
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 47c7beb4..81e13af7 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -64,17 +64,7 @@ type fun_decl_id = A.fun_decl_id [@@deriving show, ord]
this state is opaque to Aeneas (the user can define it, or leave it as
assumed)
*)
-type assumed_ty =
- | State
- | Result
- | Error
- | Fuel
- | Vec
- | Option
- | Array
- | Slice
- | Str
- | Range
+type assumed_ty = State | Result | Error | Fuel | Array | Slice | Str
[@@deriving show, ord]
(* TODO: we should never directly manipulate [Return] and [Fail], but rather