diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index 537af0103aacfd18826560b0927c959574c9f469..445ecb3af1c68ec02aac544802e0469b9cb2efec 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -142,7 +142,6 @@
         "for", (fun _ -> FOR);
         "global", (fun _ -> GLOBAL);
         "if", (fun _ -> IF);
-	"impact", (fun _ -> IMPACT);
 	"inductive", (fun _ -> INDUCTIVE);
 	"include", (fun _ -> INCLUDE);
         (* ACSL extension for external spec file *)
@@ -159,7 +158,6 @@
         (* ACSL extension for model fields *)
         "module", (fun _ -> MODULE);
         (* ACSL extension for external spec file *)
-        "pragma", (fun _ -> PRAGMA);
         "predicate", (fun _ -> PREDICATE);
         "reads", (fun _ -> READS);
         "requires", (fun _ -> REQUIRES);
@@ -167,7 +165,6 @@
         "short", (fun _ -> SHORT);
         "signed", (fun _ -> SIGNED);
         "sizeof", (fun _ -> SIZEOF);
-        "slice", (fun _ -> SLICE);
         "struct", (fun _ -> STRUCT);
         "terminates", (fun _ -> TERMINATES);
         "type", (fun _ -> TYPE);
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index e233ab3d15bda459bbaddef8ba9011cf9c9d3c50..4e8987cc60448820622a9b4d855f9b9e4d432edf 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -270,7 +270,7 @@
 %token ALLOCABLE FREEABLE FRESH
 %token DOLLAR QUESTION MINUS PLUS STAR AMP SLASH PERCENT LSQUARE RSQUARE EOF
 %token GLOBAL INVARIANT VARIANT DECREASES FOR LABEL ASSERT CHECK ADMIT SEMICOLON NULL EMPTY
-%token REQUIRES ENSURES ALLOCATES FREES ASSIGNS LOOP NOTHING SLICE IMPACT PRAGMA FROM
+%token REQUIRES ENSURES ALLOCATES FREES ASSIGNS LOOP NOTHING FROM
 %token CHECK_REQUIRES CHECK_LOOP CHECK_INVARIANT CHECK_LEMMA
 %token CHECK_ENSURES CHECK_EXITS CHECK_CONTINUES CHECK_BREAKS CHECK_RETURNS
 %token ADMIT_REQUIRES ADMIT_LOOP ADMIT_INVARIANT ADMIT_LEMMA
@@ -895,7 +895,6 @@ full_identifier:
 | FREES { "frees" }
 | FUNCTION { "function" }
 | GLOBAL { "global" }
-| IMPACT { "impact" }
 | INDUCTIVE { "inductive" }
 | INCLUDE { "include" }
 | INVARIANT { "invariant" }
@@ -905,11 +904,9 @@ full_identifier:
 | LOOP { "loop" }
 | MODEL { "model" }
 | MODULE { "module" }
-| PRAGMA { "pragma" }
 | PREDICATE { "predicate" }
 | REQUIRES { "requires" }
 | RETURNS { "returns" }
-| SLICE { "slice" }
 | TERMINATES { "terminates" }
 | TYPE { "type" }
 | VARIANT { "variant" }
@@ -1322,8 +1319,8 @@ annotation:
         Aloop_annot (loc $sloc, l) }
 | FOR ne_behavior_name_list COLON contract_or_code_annotation
       { $4 $2 }
-| pragma_or_code_annotation { Acode_annot (loc $sloc,$1) }
-| pragma_or_code_annotation beg_pragma_or_code_annotation
+| code_annotation { Acode_annot (loc $sloc,$1 []) }
+| code_annotation beg_code_annotation
       { raise
           (Not_well_formed (loc $sloc,
                             "Only one code annotation is allowed per comment"))
@@ -1458,9 +1455,7 @@ loop_grammar_extension:
 
 /*** code annotations ***/
 
-beg_pragma_or_code_annotation:
-| IMPACT {}
-| SLICE {}
+beg_code_annotation:
 | FOR {}
 | ASSERT {}
 | CHECK {}
@@ -1473,10 +1468,6 @@ beg_pragma_or_code_annotation:
 | EXT_CODE_ANNOT {}
 ;
 
-pragma_or_code_annotation:
-| code_annotation  { $1 []  }
-;
-
 code_annotation:
 | ASSERT lexpr SEMICOLON
   { fun bhvs -> AAssert (bhvs,toplevel_pred Assert $2) }
@@ -1934,7 +1925,6 @@ is_acsl_decl_or_code_annot:
 | CHECK     { "check" }
 | ADMIT     { "admit" }
 | GLOBAL    { "global" }
-| IMPACT    { "impact" }
 | INDUCTIVE { "inductive" }
 | INVARIANT { "invariant" }
 | ADMIT_INVARIANT { "admit invariant" }
@@ -1945,9 +1935,7 @@ is_acsl_decl_or_code_annot:
 | LOOP      { "loop" }
 | ADMIT_LOOP { "admit loop" }
 | CHECK_LOOP { "check loop" }
-| PRAGMA    { "pragma" }
 | PREDICATE { "predicate" }
-| SLICE     { "slice" }
 | TYPE      { "type" }
 | MODEL     { "model" }
 | AXIOM     { "axiom" }