diff options
author | Son HO | 2023-11-28 08:04:43 +0100 |
---|---|---|
committer | GitHub | 2023-11-28 08:04:43 +0100 |
commit | b78850a81dfea78bc280f1b5b6d2fdcb421e386a (patch) | |
tree | 3a4807b26856c0c2e21f1a8a4cdf80da136c26ec /compiler/Extract.ml | |
parent | bacf3f5f6f5f6a9aa650d5ae8d12a132fd747039 (diff) | |
parent | a3a3ab9723348e24f83073a52145128f34022265 (diff) |
Merge pull request #46 from AeneasVerif/son_improves
Minor improvements for the extraction
Diffstat (limited to '')
-rw-r--r-- | compiler/Extract.ml | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index c8c16c08..e48e6ae6 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -173,12 +173,7 @@ let extract_adt_g_value *) let cons = match variant_id with - | Some vid -> ( - (* In the case of Lean, we might have to add the type name as a prefix *) - match (!backend, adt_id) with - | Lean, TAssumed _ -> - ctx_get_type adt_id ctx ^ "." ^ ctx_get_variant adt_id vid ctx - | _ -> ctx_get_variant adt_id vid ctx) + | Some vid -> ctx_get_variant adt_id vid ctx | None -> ctx_get_struct adt_id ctx in let use_parentheses = inside && field_values <> [] in @@ -2723,7 +2718,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt "=="; F.pp_print_space fmt (); let success = ctx_get_variant (TAssumed TResult) result_return_id ctx in - F.pp_print_string fmt ("." ^ success ^ " ())") + F.pp_print_string fmt (success ^ " ())") | HOL4 -> F.pp_print_string fmt "val _ = assert_return ("; F.pp_print_string fmt "“"; |