summaryrefslogtreecommitdiff
path: root/cfrontend
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend')
-rw-r--r--cfrontend/C2C.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 14e345b..6386445 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -727,6 +727,7 @@ let string_of_errmsg msg =
let string_of_err = function
| CompcertErrors.MSG s -> camlstring_of_coqstring s
| CompcertErrors.CTX i -> extern_atom i
+ | CompcertErrors.CTXL i -> "" (* should not happen *)
in String.concat "" (List.map string_of_err msg)
let rec convertInit env init =