diff options
| author | Son HO | 2024-04-11 20:32:15 +0200 |
|---|---|---|
| committer | GitHub | 2024-04-11 20:32:15 +0200 |
| commit | 77d74452489f85f558efe07d72d0200c80b16444 (patch) | |
| tree | 810c6504b8e5b2fcde58841e25079d5e8c8e92ae /compiler/Extract.ml | |
| parent | 4fb9c9f655a9ffc3b4a1a717988311c057c9c599 (diff) | |
| parent | 2f8aa9b47acb5c98aed91c29b04f71099452e781 (diff) | |
Merge pull request #123 from AeneasVerif/son/clean
Cleanup the code in preparation of the nested loops
Diffstat (limited to 'compiler/Extract.ml')
| -rw-r--r-- | compiler/Extract.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 985fb470..6eeef772 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -2867,7 +2867,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 def.meta (TAssumed TResult) result_return_id ctx + ctx_get_variant def.meta (TAssumed TResult) result_ok_id ctx in F.pp_print_string fmt (success ^ " ())") | Coq -> @@ -2898,11 +2898,11 @@ 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 def.meta (TAssumed TResult) result_return_id ctx + ctx_get_variant def.meta (TAssumed TResult) result_ok_id ctx in F.pp_print_string fmt (success ^ " ())") | HOL4 -> - F.pp_print_string fmt "val _ = assert_return ("; + F.pp_print_string fmt "val _ = assert_ok ("; F.pp_print_string fmt "“"; let fun_name = ctx_get_local_function def.meta def.def_id def.loop_id ctx |