diff options
| author | Son Ho | 2023-09-17 00:30:32 +0200 |
|---|---|---|
| committer | Son Ho | 2023-09-17 00:30:32 +0200 |
| commit | d2724812981075ab7edc9cf7fb3915908024410a (patch) | |
| tree | ee8f644a1886f028da3ef903976c34c937db30e9 /compiler/ExtractBase.ml | |
| parent | 8e86ab71527de2d997b6454dc61ab80d52bfdc56 (diff) | |
Fix several issues with the extraction
Diffstat (limited to '')
| -rw-r--r-- | compiler/ExtractBase.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 4238d9af..a81ec052 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -952,7 +952,8 @@ let ctx_get (with_opaque_pre : bool) (id : id) (ctx : extraction_ctx) : string = in log#serror err; if !Config.extract_fail_hard then raise (Failure err) - else "(ERROR: \"" ^ id_to_string id ctx ^ "\")") + else + "(%%%ERROR: unknown identifier\": " ^ id_to_string id ctx ^ "\"%%%)") else let m = ctx.names_map.id_to_name in match IdMap.find_opt id m with |