From a20819f170acc6aad7b5aca2fbe53c7b3ab7e2b8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 16 Nov 2022 14:40:34 +0100
Subject: Automatically generate the Makefile and _CoqProject files in the
 tests subdirectories

---
 compiler/SymbolicToPure.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'compiler')

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) -> (
-- 
cgit v1.2.3