diff --git a/Makefile b/Makefile
index a58005b67deaca679dbf5c8088ddb589b4479fe0..a7bf2c34d9dbf78adb28ad7741dc26665534bb80 100644
--- a/Makefile
+++ b/Makefile
@@ -652,14 +652,6 @@ MLI_ONLY+=\
 	src/kernel_services/abstract_interp/lmap_sig.mli                     \
 	src/kernel_services/abstract_interp/offsetmap_bitwise_sig.mli
 
-NO_MLI+= src/kernel_internals/runtime/machdep_ppc_32.mli         \
-	src/kernel_internals/runtime/machdep_x86_16.mli         \
-	src/kernel_internals/runtime/machdep_x86_32.mli         \
-	src/kernel_internals/runtime/machdep_x86_64.mli         \
-	src/kernel_services/ast_printing/cabs_debug.mli        \
-	src/kernel_internals/parsing/logic_lexer.mli           \
-	src/kernel_internals/parsing/lexerhack.mli             \
-
 MODULES_NODOC+= src/kernel_internals/runtime/machdep_ppc_32.ml \
 	src/kernel_internals/runtime/machdep_x86_16.ml         \
 	src/kernel_internals/runtime/machdep_x86_32.ml         \
@@ -1218,8 +1210,7 @@ FILES_FOR_OCAMLDEP+= $(addsuffix /*.mli,$(FRAMAC_SRC_DIRS)) \
 	$(addsuffix /*.ml,$(FRAMAC_SRC_DIRS))
 
 MODULES_TODOC+=$(filter-out $(MODULES_NODOC),\
-	$(MLI_ONLY) $(NO_MLI:.mli=.ml) \
-	$(filter-out $(NO_MLI),\
+	$(MLI_ONLY) \
 	$(filter-out $(PLUGIN_TYPES_CMO_LIST:.cmo=.mli),$(CMO:.cmo=.mli))))
 
 ################################
diff --git a/src/kernel_internals/parsing/lexerhack.mli b/src/kernel_internals/parsing/lexerhack.mli
new file mode 100644
index 0000000000000000000000000000000000000000..e5286c4ddb43b03d0411d47e5ab77daf28012917
--- /dev/null
+++ b/src/kernel_internals/parsing/lexerhack.mli
@@ -0,0 +1,47 @@
+(****************************************************************************)
+(*                                                                          *)
+(*  Copyright (C) 2001-2003                                                 *)
+(*   George C. Necula    <necula@cs.berkeley.edu>                           *)
+(*   Scott McPeak        <smcpeak@cs.berkeley.edu>                          *)
+(*   Wes Weimer          <weimer@cs.berkeley.edu>                           *)
+(*   Ben Liblit          <liblit@cs.berkeley.edu>                           *)
+(*  All rights reserved.                                                    *)
+(*                                                                          *)
+(*  Redistribution and use in source and binary forms, with or without      *)
+(*  modification, are permitted provided that the following conditions      *)
+(*  are met:                                                                *)
+(*                                                                          *)
+(*  1. Redistributions of source code must retain the above copyright       *)
+(*  notice, this list of conditions and the following disclaimer.           *)
+(*                                                                          *)
+(*  2. Redistributions in binary form must reproduce the above copyright    *)
+(*  notice, this list of conditions and the following disclaimer in the     *)
+(*  documentation and/or other materials provided with the distribution.    *)
+(*                                                                          *)
+(*  3. The names of the contributors may not be used to endorse or          *)
+(*  promote products derived from this software without specific prior      *)
+(*  written permission.                                                     *)
+(*                                                                          *)
+(*  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS     *)
+(*  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT       *)
+(*  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS       *)
+(*  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE          *)
+(*  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,     *)
+(*  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,    *)
+(*  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;        *)
+(*  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER        *)
+(*  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT      *)
+(*  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN       *)
+(*  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE         *)
+(*  POSSIBILITY OF SUCH DAMAGE.                                             *)
+(*                                                                          *)
+(*  File modified by CEA (Commissariat à l'énergie atomique et aux          *)
+(*                        énergies alternatives)                            *)
+(*               and INRIA (Institut National de Recherche en Informatique  *)
+(*                          et Automatique).                                *)
+(****************************************************************************)
+
+val add_identifier: (string -> unit) ref
+val add_type: (string -> unit) ref
+val push_context: (unit -> unit) ref
+val pop_context: (unit -> unit) ref