summaryrefslogtreecommitdiff
path: root/src/Synthesis.ml
diff options
context:
space:
mode:
authorSon Ho2022-01-05 14:35:12 +0100
committerSon Ho2022-01-05 14:35:12 +0100
commit9f2f2340d5679dbd8219fdc7f026f80e1b3811c1 (patch)
tree0c0fa0dfab48ae0a70912fad083b3f5bd065feaa /src/Synthesis.ml
parent57a019c4b18d4f9a695f4520dd33d482abde3d5f (diff)
Remove synthesize_set_discriminant
Diffstat (limited to 'src/Synthesis.ml')
-rw-r--r--src/Synthesis.ml4
1 files changed, 0 insertions, 4 deletions
diff --git a/src/Synthesis.ml b/src/Synthesis.ml
index 51aa0882..dce40470 100644
--- a/src/Synthesis.ml
+++ b/src/Synthesis.ml
@@ -63,10 +63,6 @@ let synthesize_eval_rvalue_aggregate (aggregate_kind : E.aggregate_kind)
(ops : E.operand list) : unit =
()
-let synthesize_set_discriminant (p : E.place) (variant_id : T.VariantId.id) :
- unit =
- ()
-
let synthesize_non_local_function_call (fid : A.assumed_fun_id)
(region_params : T.erased_region list) (type_params : T.ety list)
(args : E.operand list) (dest : E.place) : unit =