diff options
| author | Son Ho | 2022-05-01 16:24:31 +0200 |
|---|---|---|
| committer | Son Ho | 2022-05-01 16:24:31 +0200 |
| commit | cfa016923779d681e639634b7e0dd16e1be9f003 (patch) | |
| tree | e58c7d96d14562e9dff454bac6af8933e1c5b153 /src/ExtractToFStar.ml | |
| parent | b664a5b1e4814a1f0105b76d5b5265e095200c3d (diff) | |
Do more cleanup
Diffstat (limited to '')
| -rw-r--r-- | src/ExtractToFStar.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 0a06ef73..068448e9 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -1475,8 +1475,8 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter) let sg = def.signature in if sg.type_params = [] - && (sg.inputs = [ unit_ty ] || sg.inputs = []) - && sg.outputs = [ mk_result_ty unit_ty ] + && (sg.inputs = [ mk_unit_ty ] || sg.inputs = []) + && sg.outputs = [ mk_result_ty mk_unit_ty ] then ( (* Add a break before *) F.pp_print_break fmt 0 0; |