summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSon Ho2022-11-16 14:40:34 +0100
committerSon HO2022-11-16 15:45:32 +0100
commita20819f170acc6aad7b5aca2fbe53c7b3ab7e2b8 (patch)
tree6818668b56b067255e874e4c9bb79ad3d52ebee7 /compiler
parentcc8cd4b9d55e21dd50fac7714203ab8a8f06242b (diff)
Automatically generate the Makefile and _CoqProject files in the tests subdirectories
Diffstat (limited to 'compiler')
-rw-r--r--compiler/SymbolicToPure.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 4ea7071b..9d8724ab 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1637,6 +1637,8 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
match branches with
| [] -> raise (Failure "Unreachable")
| [ (variant_id, svl, branch) ]
+ (* TODO: always introduce a match, and use micro-passes to turn the
+ the match into a let *)
when not
(TypesUtils.ty_is_custom_adt sv.V.sv_ty
&& !Config.always_deconstruct_adts_with_matches) -> (