diff --git a/structures.v b/structures.v
index 1db6a0d3..616cc505 100644
--- a/structures.v
+++ b/structures.v
@@ -236,7 +236,9 @@ pred docstring o:loc, o:string.
 
 (* This database is used by the parsing phase only *)
 #[synterp] Elpi Db export.db lp:{{
-  pred module-to-export o:string, o:modpath.
+  % the middle argument [id] is useless, but to preserve compat with < 8.18
+  % we keep the same signature found in hb.db
+  pred module-to-export   o:string, o:id, o:modpath.
 
 }}.
 
@@ -451,9 +453,9 @@ Elpi Accumulate File "HB/instance.elpi".
 Elpi Accumulate File "HB/context.elpi".
 Elpi Accumulate File "HB/export.elpi".
 Elpi Accumulate File "HB/factory.elpi".
-#[synterp] Elpi Accumulate File "HB/common/utils-synterp.elpi".
-#[synterp] Elpi Accumulate Db export.db.
-#[synterp] Elpi Accumulate lp:{{
+#[synterp,skip="8.1[67]"] Elpi Accumulate File "HB/common/utils-synterp.elpi".
+#[synterp,skip="8.1[67]"] Elpi Accumulate Db export.db.
+#[synterp,skip="8.1[67]"] Elpi Accumulate lp:{{
 
 pred record-decl->id i:indt-decl, o:id.
 record-decl->id (parameter _ _ _ D) N :- pi p\ record-decl->id (D p) N.
@@ -471,7 +473,7 @@ actions N :-
   end-module _,
   export-module E,
   coq.env.current-library File,
-  coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File E)).
+  coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File "" E)).
 
 main [indt-decl D] :- record-decl->id D N, with-attributes (actions N).
   
@@ -645,9 +647,9 @@ Elpi Accumulate File "HB/instance.elpi".
 Elpi Accumulate File "HB/context.elpi".
 Elpi Accumulate File "HB/factory.elpi".
 Elpi Accumulate File "HB/structure.elpi".
-#[synterp] Elpi Accumulate File "HB/common/utils-synterp.elpi".
-#[synterp] Elpi Accumulate Db export.db.
-#[synterp] Elpi Accumulate lp:{{
+#[synterp,skip="8.1[67]"] Elpi Accumulate File "HB/common/utils-synterp.elpi".
+#[synterp,skip="8.1[67]"] Elpi Accumulate Db export.db.
+#[synterp,skip="8.1[67]"] Elpi Accumulate lp:{{
 
 shorten coq.env.{ begin-module, end-module, begin-section, end-section, import-module, export-module }.
 
@@ -663,8 +665,8 @@ actions N :-
   end-module O,
   export-module O,
   coq.env.current-library File,
-  coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File E)),
-  coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File O)),
+  coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File "" E)),
+  coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File "" O)),
   if (get-option "mathcomp" tt ; get-option "mathcomp.axiom" _) (actions-compat N) true.
 
 pred actions-compat i:id.
@@ -676,7 +678,7 @@ actions-compat ModuleName :-
   end-module O,
   export-module O,
   coq.env.current-library File,
-  coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File O)).
+  coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File "" O)).
 
 main [const-decl N _ _] :- !, with-attributes (actions N).
   
@@ -768,7 +770,7 @@ Elpi Accumulate File "HB/common/log.elpi".
 Elpi Accumulate File "HB/common/synthesis.elpi".
 Elpi Accumulate File "HB/context.elpi".
 Elpi Accumulate File "HB/instance.elpi".
-#[synterp] Elpi Accumulate lp:{{
+#[synterp,skip="8.1[67]"] Elpi Accumulate lp:{{
 
 shorten coq.env.{ begin-section, end-section }.
 
@@ -813,9 +815,9 @@ Elpi Accumulate File "HB/instance.elpi".
 Elpi Accumulate File "HB/context.elpi".
 Elpi Accumulate File "HB/export.elpi".
 Elpi Accumulate File "HB/factory.elpi".
-#[synterp] Elpi Accumulate File "HB/common/utils-synterp.elpi".
-#[synterp] Elpi Accumulate Db export.db.
-#[synterp] Elpi Accumulate lp:{{
+#[synterp,skip="8.1[67]"] Elpi Accumulate File "HB/common/utils-synterp.elpi".
+#[synterp,skip="8.1[67]"] Elpi Accumulate Db export.db.
+#[synterp,skip="8.1[67]"] Elpi Accumulate lp:{{
 
 pred record-decl->id i:indt-decl, o:id.
 record-decl->id (parameter _ _ _ D) N :- pi p\ record-decl->id (D p) N.
@@ -833,7 +835,7 @@ actions N :-
   end-module _,
   export-module E,
   coq.env.current-library File,
-  coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File E)).
+  coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File "" E)).
 
 main [indt-decl D] :- record-decl->id D N, with-attributes (actions N).
 main [const-decl N _ _] :- with-attributes (actions N).
@@ -901,8 +903,8 @@ Elpi Accumulate File "HB/context.elpi".
 Elpi Accumulate File "HB/export.elpi".
 Elpi Accumulate File "HB/factory.elpi".
 Elpi Accumulate File "HB/builders.elpi".
-#[synterp] Elpi Accumulate File "HB/common/utils-synterp.elpi".
-#[synterp] Elpi Accumulate lp:{{
+#[synterp,skip="8.1[67]"] Elpi Accumulate File "HB/common/utils-synterp.elpi".
+#[synterp,skip="8.1[67]"] Elpi Accumulate lp:{{
 
 shorten coq.env.{ begin-module, end-module, begin-section }.
 
@@ -940,9 +942,9 @@ Elpi Accumulate File "HB/instance.elpi".
 Elpi Accumulate File "HB/context.elpi".
 Elpi Accumulate File "HB/export.elpi".
 Elpi Accumulate File "HB/builders.elpi".
-#[synterp] Elpi Accumulate File "HB/common/utils-synterp.elpi".
-#[synterp] Elpi Accumulate Db export.db.
-#[synterp] Elpi Accumulate lp:{{
+#[synterp,skip="8.1[67]"] Elpi Accumulate File "HB/common/utils-synterp.elpi".
+#[synterp,skip="8.1[67]"] Elpi Accumulate Db export.db.
+#[synterp,skip="8.1[67]"] Elpi Accumulate lp:{{
 
 shorten coq.env.{ end-module, end-section, begin-module, end-module, export-module }.
 
@@ -954,7 +956,7 @@ actions :-
   end-module _,
   export-module M,
   coq.env.current-library File,
-  coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File M)).
+  coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File "" M)).
 
 main [] :- !, with-attributes actions.
 main _ :- coq.error "Usage: HB.end.".
@@ -1011,9 +1013,9 @@ Elpi Accumulate File "HB/common/database.elpi".
 Elpi Accumulate File "HB/common/utils.elpi".
 Elpi Accumulate File "HB/common/log.elpi".
 Elpi Accumulate File "HB/export.elpi".
-#[synterp] Elpi Accumulate File "HB/common/utils-synterp.elpi".
-#[synterp] Elpi Accumulate Db export.db.
-#[synterp] Elpi Accumulate lp:{{
+#[synterp,skip="8.1[67]"] Elpi Accumulate File "HB/common/utils-synterp.elpi".
+#[synterp,skip="8.1[67]"] Elpi Accumulate Db export.db.
+#[synterp,skip="8.1[67]"] Elpi Accumulate lp:{{
 
 shorten coq.env.{ export-module }.
 
@@ -1021,7 +1023,7 @@ pred actions i:list located.
 actions [loc-modpath MP] :- !,
   export-module MP,
   coq.env.current-library File,
-  coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File MP)).
+  coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File "" MP)).
 actions [].
 
 main [str M] :- !, with-attributes (actions {coq.locate-all M}).
@@ -1057,14 +1059,14 @@ Elpi Accumulate File "HB/common/database.elpi".
 Elpi Accumulate File "HB/common/utils.elpi".
 Elpi Accumulate File "HB/common/log.elpi".
 Elpi Accumulate File "HB/export.elpi".
-#[synterp] Elpi Accumulate File "HB/common/utils-synterp.elpi".
-#[synterp] Elpi Accumulate Db export.db.
-#[synterp] Elpi Accumulate lp:{{
+#[synterp,skip="8.1[67]"] Elpi Accumulate File "HB/common/utils-synterp.elpi".
+#[synterp,skip="8.1[67]"] Elpi Accumulate Db export.db.
+#[synterp,skip="8.1[67]"] Elpi Accumulate lp:{{
 
 shorten coq.env.{ export-module }.
 
 pred module-in-module i:list string, i:prop.
-module-in-module PM (module-to-export _ M) :-
+module-in-module PM (module-to-export _ _ M) :-
   coq.modpath->path M PC,
   std.appendR PM _ PC. % sublist
 
@@ -1072,9 +1074,9 @@ pred actions i:option id.
 actions Filter :-
   coq.env.current-library File,
   compute-filter Filter MFilter,
-  std.findall (module-to-export File Module_) ModsCL,
+  std.findall (module-to-export File _ Module_) ModsCL,
   std.filter {list-uniq ModsCL} (module-in-module MFilter) ModsCLFiltered,
-  std.forall ModsCLFiltered (x\sigma mp\x = module-to-export _ mp, export-module mp).
+  std.forall ModsCLFiltered (x\sigma mp\x = module-to-export _ _ mp, export-module mp).
 
 main [] :- !, with-attributes (actions none).
 main [str M] :- !, with-attributes (actions (some M)).