diff options
| author | Son Ho | 2024-06-05 14:32:19 +0200 |
|---|---|---|
| committer | Son Ho | 2024-06-05 14:32:19 +0200 |
| commit | 35c6b1c3c3dbd1b782cb00206c773021f5c74765 (patch) | |
| tree | c103860afdc8c24c16ac8bbf1c705e956bf5a16a /compiler/PureMicroPasses.ml | |
| parent | baa0771885546816461e063131162b94c6954d86 (diff) | |
Add an option to run Aeneas as a borrow checker
Diffstat (limited to 'compiler/PureMicroPasses.ml')
| -rw-r--r-- | compiler/PureMicroPasses.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index a4319b28..a22a39ab 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -649,7 +649,7 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl = (* Convert, if possible - note that for now for Lean and Coq we don't support the structure syntax on recursive structures *) if - (!Config.backend <> Lean && !Config.backend <> Coq) + (Config.backend () <> Lean && Config.backend () <> Coq) || not is_rec then let struct_id = TAdtId adt_id in @@ -1295,7 +1295,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl = the shape [{ x with f := v }]). This is not supported by Coq *) - !Config.backend <> Coq + Config.backend () <> Coq then ( (* Compute the number of occurrences of each variable *) let occurs = ref VarId.Map.empty in |