diff --git a/dev/docker/Dockerfile b/dev/docker/Dockerfile
index 2ee81468180c2b4b6409b8e99e890fc81472d184..96e366bce95cdb40b26007f7b525701c4b407d30 100644
--- a/dev/docker/Dockerfile
+++ b/dev/docker/Dockerfile
@@ -281,7 +281,6 @@ RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/lib/alt-ergo
 RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/lib/lablgtk3
 RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/lib/lablgtk3-sourceview3
 RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/lib/ppx_deriving
-RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/lib/ppx_import
 RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/lib/ppx_tools
 RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/lib/ppxlib
 RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/lib/psmt2-frontend
diff --git a/nix/frama-c.nix b/nix/frama-c.nix
index 62ca10893d07216c6b1d7e155eab94fce8986321..bdf835c48ff6e431cbdbcad714d56606ac53be05 100644
--- a/nix/frama-c.nix
+++ b/nix/frama-c.nix
@@ -39,7 +39,6 @@
 , ppx_deriving
 , ppx_deriving_yaml
 , ppx_deriving_yojson
-, ppx_import
 , unionFind
 , yojson
 , which
@@ -101,7 +100,6 @@ stdenvNoCC.mkDerivation rec {
     ppx_deriving
     ppx_deriving_yaml
     ppx_deriving_yojson
-    ppx_import
     unionFind
     yojson
     which
diff --git a/nix/internal-tests.nix b/nix/internal-tests.nix
index 48e04ae1ac9118583330ef6b08b856f875d7ac2c..67fae7c79d84c1327fb351366f0fad4a67d92d95 100644
--- a/nix/internal-tests.nix
+++ b/nix/internal-tests.nix
@@ -33,7 +33,6 @@
 , ppx_deriving
 , ppx_deriving_yaml
 , ppx_deriving_yojson
-, ppx_import
 , unionFind
 , yojson
 , which
@@ -96,7 +95,6 @@ stdenvNoCC.mkDerivation rec {
     ppx_deriving
     ppx_deriving_yaml
     ppx_deriving_yojson
-    ppx_import
     unionFind
     yojson
     which
diff --git a/opam b/opam
index 8553ce6ee227c1ba56ed079f4269024f7e5b91fd..baf369d4a97a82ba39f1602b41ce6ad132eac593 100644
--- a/opam
+++ b/opam
@@ -145,7 +145,6 @@ depends: [
   "ppx_deriving"
   "ppx_deriving_yojson"
   "ppx_deriving_yaml" { >= "0.2.0" }
-  "ppx_import"
 
   # GTK3 disabled on macOS (segfaults), and made optional on Windows
   # (due to complex situation with Cygwin + MinGW).
diff --git a/reference-configuration.md b/reference-configuration.md
index 5ba397866c50985d0bdb5339e4d27166b587467a..1ec28fc3b93adcc1644d5220da2172424685008b 100644
--- a/reference-configuration.md
+++ b/reference-configuration.md
@@ -13,7 +13,6 @@ compiling Frama-C 28.1.
 - ocamlgraph.2.1.0
 - ppx_deriving_yaml.0.2.1
 - ppx_deriving_yojson.3.7.0
-- ppx_import.1.10.0
 - unionFind.20220122
 - why3.1.6.0
 - yojson.2.0.2
diff --git a/src/dune b/src/dune
index 1df313dfe3b14cf5b89e8942fcd3e73b1a2e9e23..4e30a8be96104f936abe77828007e05be04e3a6e 100644
--- a/src/dune
+++ b/src/dune
@@ -37,7 +37,6 @@
           (echo "  - menhirLib:" %{lib-available:menhirLib} "\n")
           (echo "  - dune-site:" %{lib-available:dune-site} "\n")
           (echo "  - dune-site.plugins:" %{lib-available:dune-site.plugins} "\n")
-          (echo "  - ppx_import:" %{lib-available:ppx_import} "\n")
           (echo "  - ppx_deriving.eq:" %{lib-available:ppx_deriving.eq} "\n")
           (echo "  - ppx_deriving.ord:" %{lib-available:ppx_deriving.ord} "\n")
           (echo "  - ppx_deriving_yaml:" %{lib-available:ppx_deriving_yaml} "\n")
@@ -53,7 +52,7 @@
   (libraries frama-c.init fpath str unix zarith ocamlgraph dynlink bytes yaml.unix yojson menhirLib dune-site dune-site.plugins)
   (instrumentation (backend landmarks))
   (instrumentation (backend bisect_ppx))
-  (preprocess (staged_pps ppx_import ppx_deriving.eq ppx_deriving.ord ppx_deriving_yaml))
+  (preprocess (pps ppx_deriving.eq ppx_deriving.ord ppx_deriving_yaml))
 )
 
 (generate_sites_module (module config_data) (sites frama-c) (plugins (frama-c plugins) (frama-c plugins_gui)))
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index 9fb991e9eccd6b53dff7da97314be358c63f6f54..0b27f448cc4937d02c715c9f40ba63603e12ac99 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -54,6 +54,118 @@
 (* check_file class in frama-c/src/file.ml (before launching the tests)     *)
 (****************************************************************************)
 
+(* ************************************************************************* *)
+(** {2 Simple types} *)
+(* ************************************************************************* *)
+
+(* ************************************************************************* *)
+(** {3 Operators} *)
+(* ************************************************************************* *)
+
+(** Unary operators *)
+type unop =
+  | Neg   (** Unary minus *)
+  | BNot  (** Bitwise complement (~) *)
+  | LNot  (** Logical Not (!) *)
+[@@deriving eq]
+
+(** Binary operations *)
+type binop =
+    PlusA    (** arithmetic + *)
+  | PlusPI   (** pointer + integer *)
+  | MinusA   (** arithmetic - *)
+  | MinusPI  (** pointer - integer *)
+  | MinusPP  (** pointer - pointer *)
+  | Mult     (** * *)
+  | Div      (** /
+                 @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
+  | Mod      (** %
+                 @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
+  | Shiftlt  (** shift left *)
+  | Shiftrt  (** shift right *)
+
+  | Lt       (** <  (arithmetic comparison) *)
+  | Gt       (** >  (arithmetic comparison) *)
+  | Le       (** <= (arithmetic comparison) *)
+  | Ge       (** >= (arithmetic comparison) *)
+  | Eq       (** == (arithmetic comparison) *)
+  | Ne       (** != (arithmetic comparison) *)
+  | BAnd     (** bitwise and *)
+  | BXor     (** exclusive-or *)
+  | BOr      (** inclusive-or *)
+
+  | LAnd     (** logical and. Unlike other expressions this one does not always
+                 evaluate both operands. If you want
+                 to use these, you must set
+                 {!Cil.useLogicalOperators}. *)
+  | LOr      (** logical or. Unlike other expressions this one does not always
+                 evaluate both operands.  If you
+                 want to use these, you must set
+                 {!Cil.useLogicalOperators}. *)
+[@@deriving eq]
+
+(* ************************************************************************* *)
+(** {3 Types} *)
+(* ************************************************************************* *)
+
+(** Various kinds of integers *)
+type ikind =
+  | IBool       (** [_Bool] *)
+  | IChar       (** [char] *)
+  | ISChar      (** [signed char] *)
+  | IUChar      (** [unsigned char] *)
+  | IInt        (** [int] *)
+  | IUInt       (** [unsigned int] *)
+  | IShort      (** [short] *)
+  | IUShort     (** [unsigned short] *)
+  | ILong       (** [long] *)
+  | IULong      (** [unsigned long] *)
+  | ILongLong   (** [long long] (or [_int64] on Microsoft Visual C) *)
+  | IULongLong  (** [unsigned long long] (or [unsigned _int64] on MSVC) *)
+[@@deriving eq]
+
+(** Various kinds of floating-point numbers*)
+type fkind =
+  | FFloat      (** [float] *)
+  | FDouble     (** [double] *)
+  | FLongDouble (** [long double] *)
+[@@deriving eq]
+
+(* ************************************************************************* *)
+(** {3 Logic} *)
+(* ************************************************************************* *)
+
+type predicate_kind = Assert | Check | Admit
+[@@deriving eq]
+
+(** builtin logic labels defined in ACSL. *)
+type logic_builtin_label =
+  | Here
+  | Old
+  | Pre
+  | Post
+  | LoopEntry
+  | LoopCurrent
+  | Init
+[@@deriving eq]
+
+(** comparison relations*)
+type relation =
+  | Rlt
+  | Rgt
+  | Rle
+  | Rge
+  | Req
+  | Rneq
+  (** Different
+      @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
+  *)
+[@@deriving eq]
+
+(** kind of termination a post-condition applies to. See ACSL manual. *)
+type termination_kind = Normal | Exits | Breaks | Continues | Returns
+[@@deriving eq]
+
 (* ************************************************************************* *)
 (** {2 Root of the AST} *)
 (* ************************************************************************* *)
@@ -243,28 +355,6 @@ and typ =
   | TBuiltin_va_list of attributes
   (** This is the same as the gcc's type with the same name *)
 
-(** Various kinds of integers *)
-and ikind =
-    IBool       (** [_Bool] *)
-  | IChar       (** [char] *)
-  | ISChar      (** [signed char] *)
-  | IUChar      (** [unsigned char] *)
-  | IInt        (** [int] *)
-  | IUInt       (** [unsigned int] *)
-  | IShort      (** [short] *)
-  | IUShort     (** [unsigned short] *)
-  | ILong       (** [long] *)
-  | IULong      (** [unsigned long] *)
-  | ILongLong   (** [long long] (or [_int64] on Microsoft Visual C) *)
-  | IULongLong  (** [unsigned long long] (or [unsigned _int64] on Microsoft
-                    Visual C) *)
-
-(** Various kinds of floating-point numbers*)
-and fkind =
-    FFloat      (** [float] *)
-  | FDouble     (** [double] *)
-  | FLongDouble (** [long double] *)
-
 (* ************************************************************************* *)
 (** {2 Attributes} *)
 (* ************************************************************************* *)
@@ -742,46 +832,6 @@ and constant =
   (** An enumeration constant. Use [Cillower.lowerEnumVisitor] to replace these
       with integer constants. *)
 
-(** Unary operators *)
-and unop =
-    Neg   (** Unary minus *)
-  | BNot  (** Bitwise complement (~) *)
-  | LNot  (** Logical Not (!) *)
-
-(** Binary operations *)
-and binop =
-    PlusA    (** arithmetic + *)
-  | PlusPI   (** pointer + integer *)
-  | MinusA   (** arithmetic - *)
-  | MinusPI  (** pointer - integer *)
-  | MinusPP  (** pointer - pointer *)
-  | Mult     (** * *)
-  | Div      (** /
-                 @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
-  | Mod      (** %
-                 @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
-  | Shiftlt  (** shift left *)
-  | Shiftrt  (** shift right *)
-
-  | Lt       (** <  (arithmetic comparison) *)
-  | Gt       (** >  (arithmetic comparison) *)
-  | Le       (** <= (arithmetic comparison) *)
-  | Ge       (** >= (arithmetic comparison) *)
-  | Eq       (** == (arithmetic comparison) *)
-  | Ne       (** != (arithmetic comparison) *)
-  | BAnd     (** bitwise and *)
-  | BXor     (** exclusive-or *)
-  | BOr      (** inclusive-or *)
-
-  | LAnd     (** logical and. Unlike other expressions this one does not always
-                 evaluate both operands. If you want
-                 to use these, you must set
-                 {!Cil.useLogicalOperators}. *)
-  | LOr      (** logical or. Unlike other expressions this one does not always
-                 evaluate both operands.  If you
-                 want to use these, you must set
-                 {!Cil.useLogicalOperators}. *)
-
 (* ************************************************************************* *)
 (** {2 Left values} *)
 (* ************************************************************************* *)
@@ -1321,16 +1371,6 @@ and logic_label =
   | FormalLabel of string (** label of global annotation. *)
   | BuiltinLabel of logic_builtin_label
 
-(** builtin logic labels defined in ACSL. *)
-and logic_builtin_label =
-  | Here
-  | Old
-  | Pre
-  | Post
-  | LoopEntry
-  | LoopCurrent
-  | Init
-
 (* ************************************************************************* *)
 (** {2 Terms} *)
 (* ************************************************************************* *)
@@ -1523,19 +1563,6 @@ and logic_ctor_info =
 (** variables bound by a quantifier. *)
 and quantifiers = logic_var list
 
-(** comparison relations*)
-and relation =
-  | Rlt
-  | Rgt
-  | Rle
-  | Rge
-  | Req
-  | Rneq
-  (** Different
-      @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
-  *)
-
-
 (** predicates *)
 and predicate_node =
   | Pfalse (** always-false predicate. *)
@@ -1578,11 +1605,6 @@ and identified_predicate = {
   ip_content: toplevel_predicate; (** the predicate itself*)
 }
 
-and predicate_kind =
-  | Assert
-  | Check
-  | Admit
-
 (** main statement of an annotation. *)
 and toplevel_predicate = {
   tp_kind: predicate_kind;
@@ -1713,9 +1735,6 @@ and behavior = {
   (** extensions *)
 }
 
-(** kind of termination a post-condition applies to. See ACSL manual. *)
-and termination_kind = Normal | Exits | Breaks | Continues | Returns
-
 (** Pragmas for the value analysis plugin of Frama-C. *)
 and loop_pragma =
   | Unroll_specs of term list
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 3b73ea2acc6ee7008575ff226599c2d6a29fb22e..7bd699ec2467e1e631d63c7d35f3a737dc4c0a8a 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -439,35 +439,35 @@ let is_matching_logic_type_var a a' env =
   | Some a'' -> Datatype.String.equal a' a''
 
 module Unop = struct
-  type t = [%import: Cil_types.unop] [@@deriving eq]
+  type t = Cil_types.unop [@@deriving eq]
 end
 
 module Binop = struct
-  type t = [%import: Cil_types.binop] [@@deriving eq]
+  type t = Cil_types.binop [@@deriving eq]
 end
 
 module Ikind = struct
-  type t = [%import: Cil_types.ikind] [@@deriving eq]
+  type t = Cil_types.ikind [@@deriving eq]
 end
 
 module Fkind = struct
-  type t = [%import: Cil_types.fkind] [@@deriving eq]
+  type t = Cil_types.fkind [@@deriving eq]
 end
 
 module Predicate_kind = struct
-  type t = [%import: Cil_types.predicate_kind] [@@deriving eq]
+  type t = Cil_types.predicate_kind [@@deriving eq]
 end
 
 module Logic_builtin_label = struct
-  type t = [%import: Cil_types.logic_builtin_label] [@@deriving eq]
+  type t = Cil_types.logic_builtin_label [@@deriving eq]
 end
 
 module Relation = struct
-  type t = [%import: Cil_types.relation] [@@deriving eq]
+  type t = Cil_types.relation [@@deriving eq]
 end
 
 module Termination_kind = struct
-  type t = [%import: Cil_types.termination_kind] [@@deriving eq]
+  type t = Cil_types.termination_kind [@@deriving eq]
 end
 
 let is_same_behavior_set l l' =
diff --git a/src/plugins/eva/dune b/src/plugins/eva/dune
index ee102c636e8dba81c0523c333d5ca81ca3984577..71e32bff86870737e824723a07bf73d9859024ec 100644
--- a/src/plugins/eva/dune
+++ b/src/plugins/eva/dune
@@ -45,7 +45,7 @@
  (libraries frama-c.kernel frama-c-server.core frama-c-postdominators.core)
  (instrumentation (backend landmarks))
  (instrumentation (backend bisect_ppx))
- (preprocess (staged_pps ppx_deriving.eq ppx_deriving.ord)))
+ (preprocess (pps ppx_deriving.eq ppx_deriving.ord)))
 
 (plugin
  (name eva)