diff options
| author | Son Ho | 2022-01-05 14:35:12 +0100 |
|---|---|---|
| committer | Son Ho | 2022-01-05 14:35:12 +0100 |
| commit | 9f2f2340d5679dbd8219fdc7f026f80e1b3811c1 (patch) | |
| tree | 0c0fa0dfab48ae0a70912fad083b3f5bd065feaa /src/Interpreter.ml | |
| parent | 57a019c4b18d4f9a695f4520dd33d482abde3d5f (diff) | |
Remove synthesize_set_discriminant
Diffstat (limited to '')
| -rw-r--r-- | src/Interpreter.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 970ef3a6..482a3623 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -3521,7 +3521,6 @@ let rec end_loan_exactly_at_place (config : C.config) (access : access_kind) *) let set_discriminant (config : C.config) (ctx : C.eval_ctx) (p : E.place) (variant_id : T.VariantId.id) : C.eval_ctx * statement_eval_res = - S.synthesize_set_discriminant p variant_id; (* Access the value *) let access = Write in let ctx = update_ctx_along_read_place config access p ctx in |