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/ExtractBase.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/ExtractBase.ml')
| -rw-r--r-- | compiler/ExtractBase.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 47b613c2..656d2f27 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1020,7 +1020,7 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list = match !backend with | FStar -> [ - (TResult, result_return_id, "Return"); + (TResult, result_ok_id, "Ok"); (TResult, result_fail_id, "Fail"); (TError, error_failure_id, "Failure"); (TError, error_out_of_fuel_id, "OutOfFuel"); @@ -1029,7 +1029,7 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list = ] | Coq -> [ - (TResult, result_return_id, "Return"); + (TResult, result_ok_id, "Ok"); (TResult, result_fail_id, "Fail_"); (TError, error_failure_id, "Failure"); (TError, error_out_of_fuel_id, "OutOfFuel"); @@ -1038,7 +1038,7 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list = ] | Lean -> [ - (TResult, result_return_id, "Result.ret"); + (TResult, result_ok_id, "Result.ok"); (TResult, result_fail_id, "Result.fail"); (* For panic: we omit the prefix "Error." because the type is always clear from the context. Also, "Error" is often used by user-defined @@ -1049,7 +1049,7 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list = ] | HOL4 -> [ - (TResult, result_return_id, "Return"); + (TResult, result_ok_id, "Ok"); (TResult, result_fail_id, "Fail"); (TError, error_failure_id, "Failure"); (* No Fuel::Zero on purpose *) |