diff options
| author | Son HO | 2024-06-11 14:36:40 +0200 |
|---|---|---|
| committer | GitHub | 2024-06-11 14:36:40 +0200 |
| commit | e60d525fe3dffa035d2a551af624747dca6e1c1e (patch) | |
| tree | d7b06e270fd6a1cf69717f98db7c30e43788dad1 /compiler/SymbolicToPure.ml | |
| parent | 73e27b142b65ec37fbbc55a5a7d0299555b2b60b (diff) | |
| parent | 2e91b90e332c473253c2ff91fd65da34eb709572 (diff) | |
Merge pull request #237 from AeneasVerif/son/tuples
Do not use tuple projectors in the Lean backend
Diffstat (limited to 'compiler/SymbolicToPure.ml')
| -rw-r--r-- | compiler/SymbolicToPure.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 3975107a..87f1128d 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -2916,7 +2916,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value) at once (`let (a, b, c) = x in`) *) || TypesUtils.type_decl_from_type_id_is_tuple_struct ctx.type_ctx.type_infos type_id - && not (Config.backend_has_tuple_projectors ()) + && not !Config.use_tuple_projectors in if use_let_with_cons then (* Introduce a let binding which expands the ADT *) |