From 5f7f89c7945b82b42cf65a3570312467abe6f638 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Tue, 10 Sep 2024 12:33:59 +0200
Subject: [PATCH] [kernel] raise exception instead of abort, avoid assert false
when printing
---
src/kernel_internals/parsing/logic_lexer.mll | 12 +-----------
1 file changed, 1 insertion(+), 11 deletions(-)
diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index 2a3d39798e..70a9d8cc29 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -305,13 +305,6 @@
| ADMIT, LEMMA -> true, ADMIT_LEMMA
| _ -> false, current
- let type_to_string = function
- | TYPENAME s -> s
- | REAL -> "real"
- | BOOLEAN -> "boolean"
- | INTEGER -> "integer"
- | _ -> assert false
-
let check_ext_plugin source plugin tok =
match tok with
| IDENTIFIER s ->
@@ -335,10 +328,7 @@
Kernel.abort ~source
"Extension '%s' is from %s and not %s" s plugin_from plugin;
tok
- | _ ->
- Kernel.abort ~source
- "Type token \'%s\' received instead of extension identifier"
- (type_to_string tok)
+ | _ -> raise Parsing.Parse_error
}
let space = [' ' '\t' '\012' '\r' '@' ]
--
GitLab