From 5dd3ce6a545b2cec686be7ed316bd68fc17b04d4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 6 Sep 2024 14:03:18 +0200
Subject: [PATCH] [logic] restrict module identifiers to exclude keywords

---
 src/kernel_internals/parsing/logic_parser.mly | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index f2b23a2738..eed9555e41 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -1684,11 +1684,11 @@ logic_def:
     { pop_module_types () ; LDmodule($2,$4) }
 | IMPORT mId = module_name SEMICOLON
     { LDimport(None,mId,None) }
-| IMPORT mId = module_name AS id = identifier SEMICOLON
+| IMPORT mId = module_name AS id = IDENTIFIER SEMICOLON
     { LDimport(None,mId,Some id) }
-| IMPORT drv = identifier COLON mId = module_name SEMICOLON
+| IMPORT drv = IDENTIFIER COLON mId = module_name SEMICOLON
     { LDimport(Some drv,mId,None) }
-| IMPORT drv = identifier COLON mId = module_name AS id = identifier SEMICOLON
+| IMPORT drv = IDENTIFIER COLON mId = module_name AS id = IDENTIFIER SEMICOLON
     { LDimport(Some drv,mId,Some id) }
 | TYPE poly_id_type_add_typename EQUAL typedef SEMICOLON
         { let (id,tvars) = $2 in
@@ -1698,7 +1698,7 @@ logic_def:
 ;
 
 module_name:
-| identifier { $1 }
+| IDENTIFIER { $1 }
 | LONGIDENT  { $1 }
 ;
 
-- 
GitLab