diff --git a/HB/about.elpi b/HB/about.elpi
index df48f949..e07c94fc 100644
--- a/HB/about.elpi
+++ b/HB/about.elpi
@@ -1,6 +1,9 @@
 /*        Hierarchy Builder: algebraic hierarchies made easy
     This software is released under the terms of the MIT license              */
 
+accumulate HB/common/database.
+accumulate HB/common/log.
+
 namespace about {
 
 func main string ->.
diff --git a/HB/builders.elpi b/HB/builders.elpi
index 56aeec11..038dbb8a 100644
--- a/HB/builders.elpi
+++ b/HB/builders.elpi
@@ -1,6 +1,12 @@
 /*        Hierarchy Builder: algebraic hierarchies made easy
     This software is released under the terms of the MIT license              */
 
+accumulate HB/common/database.
+accumulate HB/common/log.
+accumulate HB/context.
+accumulate HB/export.
+accumulate HB/factory.
+
 namespace builders {
 
 func begin context-decl ->.
@@ -65,8 +71,6 @@ builders.end :- std.do! [
 /* ----------------------------- private code ------------------------------ */
 /* ------------------------------------------------------------------------- */
 
-func factory.cdecl->w-mixins context-decl -> w-mixins context-decl.
-
 namespace builders.private {
 
 % [declare-1-builder (builder _ F M B) From MoreFrom] Given B of type FB, it
diff --git a/HB/check.elpi b/HB/check.elpi
new file mode 100644
index 00000000..ef85bfa6
--- /dev/null
+++ b/HB/check.elpi
@@ -0,0 +1,16 @@
+accumulate HB/common/database.
+accumulate HB/common/log.
+
+pred check-or-not i:term.
+check-or-not Skel :-
+  coq.version VersionString _ _ _,
+  if (get-option "skip" R, rex_match R VersionString)
+     (coq.warning "HB" "HB.skip" {get-option "elpi.loc"} "Skipping test on Coq" VersionString "as requested")
+     (log.coq.check Skel Ty T Result,
+      if (Result = error Msg)
+         (if (get-option "fail" tt)
+             (coq.say "The command did fail as expected with message:" Msg)
+             (coq.error "HB.check:" Msg))
+         (if (get-option "fail" tt)
+             (coq.error "The command did not fail")
+             (coq.say "HB.check:" {coq.term->string T} ":" {coq.term->string Ty}))).
diff --git a/HB/common/compat_acc_clauses_all.elpi b/HB/common/compat_acc_clauses_all.elpi
deleted file mode 100644
index 381970f8..00000000
--- a/HB/common/compat_acc_clauses_all.elpi
+++ /dev/null
@@ -1,3 +0,0 @@
-:index (1)
-func acc-clauses scope, list prop.
-acc-clauses Scope CL :- coq.elpi.accumulate-clauses Scope "hb.db" {std.map CL (c\r\ r = clause _ _ c)}.
diff --git a/HB/common/compat_add_secvar_all.elpi b/HB/common/compat_add_secvar_all.elpi
deleted file mode 100644
index 923a4f70..00000000
--- a/HB/common/compat_add_secvar_all.elpi
+++ /dev/null
@@ -1,12 +0,0 @@
-func log.coq.env.add-section-variable-noimplicits id, term -> constant.
-log.coq.env.add-section-variable-noimplicits Name Ty C :-
-  if (Name = "_") (ID is "fresh_name_" ^ {std.any->string {new_int}}) (ID = Name),
-% elpi:if version coq-elpi < 2.4.0
-  @local! => coq.env.add-section-variable ID Ty C,
-% elpi:endif
-% elpi:if version coq-elpi >= 2.4.0
-  @local! => coq.env.add-section-variable ID _ Ty C,
-% elpi:endif
-  log.private.log-vernac (log.private.coq.vernac.variable ID Ty),
-  @local! => log.coq.arguments.set-implicit (const C) [[]].
-
diff --git a/HB/common/database.elpi b/HB/common/database.elpi
index 2ecaf7ae..486addfd 100644
--- a/HB/common/database.elpi
+++ b/HB/common/database.elpi
@@ -1,6 +1,9 @@
 /*        Hierarchy Builder: algebraic hierarchies made easy
     This software is released under the terms of the MIT license              */
 
+accumulate HB/common/database_signature.
+accumulate HB/common/utils.
+
 shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }.
 
 %%%%%%%%% HB database %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/HB/common/database_signature.elpi b/HB/common/database_signature.elpi
new file mode 100644
index 00000000..3588485d
--- /dev/null
+++ b/HB/common/database_signature.elpi
@@ -0,0 +1,188 @@
+typeabbrev mixinname   gref.
+typeabbrev classname   gref.
+typeabbrev factoryname gref.
+typeabbrev structure   gref.
+
+typeabbrev (w-args A) (triple A (list term) term).
+
+kind w-params type -> type.
+type w-params.cons id -> term -> (term -> w-params A) -> w-params A.
+type w-params.nil id -> term -> (term -> A) -> w-params A.
+
+typeabbrev (list-w-params A) (w-params (list (w-args A))).
+typeabbrev (one-w-params A) (w-params (w-args A)).
+typeabbrev mixins (list-w-params mixinname).
+typeabbrev factories (list-w-params mixinname).
+typeabbrev (w-mixins A) (pair mixins (w-params A)).
+
+%%%%% Classes %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% (class C S ML) represents a class C packed in S containing mixins ML.
+% Example:
+%
+%  HB.mixin Record IsZmodule V := { ... }
+%  HB.mixin Record Zmodule_IsLmodule (R : ringType) V of Zmodule V := { ... }
+%  HB.structure Definition Lmodule R := {M of Zmodule M & Zmodule_IsLmodule R M}
+%
+% The class description for Lmodule would be:
+%
+%  class (indt «Lmodule.axioms»)                   /* The record with all mixins     */
+%        (indt «Lmodule.type»)                     /* The record with sort and class */
+%        (w-params.cons "R" {{ Ring.type }} P \    /* The first parameter, named "R" */
+%          w-params.nil "M" {{ Type }} T \         /* The key of the structure       */
+%           [...,                                  /* deps of IsZmodule.mixin        */
+%            triple (indt «IsZmodule.mixin») [] T, /* a mixins with its params       */
+%            triple (indt «Zmodule_IsLmodule.mixin») [P] T ]) /* another mixins      */
+%
+% If some mixin parameters depend on other mixins (through a canonical instance that
+% can be inferred from them). Since our structure does not account for dependencies
+% between mixins (the list in the end is flat), we compensate by replacing canonical
+% instances by calls to `S.Pack T {{lib:elpi.hole}}`, and extending the reconstruction
+% mecanism of mixins to also reinfer these holes.
+
+kind hbclass type.
+type class classname -> structure -> mixins -> hbclass.
+
+% class-def contains all the classes ever declared
+pred class-def o:hbclass.
+
+%%%%% Builders %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% [from FN MN F] invariant:
+% "F : forall p1 .. pn T LMN, FN p1 .. pn T LMN1 -> MN c1 .. cm T LMN2" where
+%  - LMN1 and LMN2 are sub lists of LMN
+%  - c1 .. cm are terms built using p1 .. pn and T
+% - [factory-requires FN LMN]
+% [from _ M _] tests whether M is a declared mixin.
+pred from o:factoryname, o:mixinname, o:gref.
+
+%%%%% Abbreviations %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% [phant-abbrev Cst AbbrevCst Abbrev]
+% Stores phantom abbreviation Abbrev associated with Cst
+% AbbrevCst is the constant that serves as support
+% e.g. Definition AbbrevCst := fun t1 t2 (phant_id t1 t2) => Cst t2.
+%      Notation   Abbrev t1 := (AbbrevCst t1 _ idfun).
+pred phant-abbrev o:gref, o:gref, o:abbreviation.
+
+% [factory-alias->gref X GR] when X is already a factory X = GR
+% however, when X is a phantom abbreviated gref, we find the underlying
+% factory gref GR associated to it.
+func factory-alias->gref gref -> gref, diagnostic.
+factory-alias->gref PhGR GR ok :- phant-abbrev GR PhGR _, !.
+factory-alias->gref GR GR ok :- phant-abbrev GR _ _, !.
+factory-alias->gref GR _ (error Msg) :- !,
+  Msg is {coq.term->string (global GR)} ^
+         " is not a factory or its library (" ^
+        { std.string.concat "." {std.drop-last 1 {coq.gref->path GR} } } ^
+        ") was not correctly imported".
+
+%%%%% Cache of known facts %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% [factory->constructor F K] means K is a constructor for
+% the factory F.
+:index(2)
+func factory->constructor factoryname -> gref.
+
+% [factory->nparams F N] says that F has N parameters
+:index(2)
+func factory->nparams factoryname -> int.
+
+% [is-structure GR] tests if GR is a known structure
+pred is-structure o:gref.
+
+% [is-factory GR] tests if GR is a known factory
+pred is-factory o:gref.
+
+% [sub-class C1 C2 Coercion12 NparamsCoercion] C1 is a sub-class of C2,
+% see also sub-class? which computes it on the fly
+:index (2 2 1)
+pred sub-class o:classname, o:classname, o:constant, o:int.
+
+% [gref->deps GR MLwP] is a (pre computed) list of dependencies of a know global
+% constant. The list is topologically sorted
+:index(2)
+func gref->deps gref -> mixins.
+
+% [join C1 C2 C3] means that C3 inherits from both C1 and C2
+pred join o:classname, o:classname, o:classname.
+
+% Section local memory of names for mixins, so that we can reuse them
+% and build terms with simpler conversion problems (less unfolding
+% in order to discover two mixins are the same)
+% @gares : is it really a func. Ideally I think so, bu we load mixin-mem via
+% `Clauses =>` in infer-class. Should perform a dynamic check?
+func mixin-mem term -> gref.
+
+%%%%%% Memory of exported mixins (HB.structure) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Operations (named mixin fields) need to be exported exactly once,
+% but the same mixin can be used in many structure, hence this memory
+% to keep the invariant.
+% Also we remember which is the first class/structure that includes
+% a given mixin, assuming the invariant that this first class is also
+% the minimal class that includes this mixin.
+% [mixin->first-class M C] states that C is the first/minimal class
+% that contains the mixin M
+:index(2)
+func mixin->first-class mixinname -> classname.
+
+% memory of exported operations (TODO: document fiels)
+pred exported-op o:mixinname, o:constant, o:constant.
+
+% memory of factory sort coercion
+pred factory-sort o:coercion.
+
+% memory of canonical projections for a structure (X.sort, X.class, X.type)
+pred structure-key o:constant, o:constant, o:structure.
+
+%%%%%% Membership of mixins to a  class %%%%%%%%%%%%%%%%
+% [mixin-class M C] means M belongs to C
+pred mixin-class o:mixinname, o:classname.
+
+%% database for HB.context %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% [mixin-src T M X] states that X can be used to reconstruct
+% an instance of the mixin [M T …], directly or through a builder.
+% Since HB.builders sections can declare canonical instances of
+% mixins that do not yet form a structure, we cannot resort to
+% Coq's CS database (which is just for structures).
+pred mixin-src o:term, o:mixinname, o:term.
+
+% [has-mixin-instance K M G] states that G is a reference to an instance
+% of mixin M for subject K
+pred has-mixin-instance o:cs-pattern, o:mixinname, o:gref.
+
+%% database for HB.builders %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% [builder N TheFactory TheMixin S] is used to
+% remember that the user run [HB.instance S] hence [HB.end] has to
+% synthesize builders from TheFactory to TheMixin mixins generated by S.
+% N is a timestamp.
+kind builder type.
+type builder int -> factoryname -> mixinname -> gref -> builder.
+pred builder-decl o:builder.
+
+%% database for builder-local canonical instances %%%%%%%%%%%%%%%%%%%%%%%
+pred local-canonical o:constant.
+
+% To tell HB.end what we are doing
+kind declaration type.
+% TheType, TheFactory and it's name and the name of the module encloding all that
+type builder-from term -> term -> factoryname -> id -> declaration.
+type no-builder declaration.
+pred current-mode o:declaration.
+
+%% database for HB.export / HB.reexport %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% library, nice-name, object
+pred module-to-export   o:string, o:id, o:modpath.
+pred instance-to-export o:string, o:id, o:constant.
+pred abbrev-to-export   o:string, o:id, o:gref.
+pred clause-to-export   o:string, o:prop.
+
+%% database for HB.locate and HB.about %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+pred decl-location o:gref, o:loc.
+
+% [docstring Loc Doc] links a location in the source text and some doc
+pred docstring o:loc, o:string.
diff --git a/HB/common/log.elpi b/HB/common/log.elpi
index 6f123d15..aacd6814 100644
--- a/HB/common/log.elpi
+++ b/HB/common/log.elpi
@@ -8,6 +8,8 @@
 %   were logging takes place. Hence we never call, say, coq.evn.add-* directly,
 %   but always via this proxy
 
+accumulate HB/common/database.
+
 namespace log.coq {
 
 :index (1)
@@ -159,6 +161,13 @@ coercion.declare C :- std.do! [
 ]. 
 
 
+func env.add-section-variable-noimplicits id, term -> constant.
+env.add-section-variable-noimplicits Name Ty C :-
+  if (Name = "_") (ID is "fresh_name_" ^ {std.any->string {new_int}}) (ID = Name),
+  @local! ==> coq.env.add-section-variable ID _ Ty C,
+  log.private.log-vernac (log.private.coq.vernac.variable ID Ty),
+  @local! ==> arguments.set-implicit (const C) [[]].
+
 }
 
 % Since CS.foo is not a valid predicate name we can't use it
diff --git a/HB/common/phant-abbreviation.elpi b/HB/common/phant-abbreviation.elpi
index 708d1a0b..d27ef6b9 100644
--- a/HB/common/phant-abbreviation.elpi
+++ b/HB/common/phant-abbreviation.elpi
@@ -11,6 +11,10 @@
 %
 % See /Canonical Structures for the working Coq user/ by Mahboubi and Tassi
 
+accumulate HB/common/database.
+accumulate HB/common/synthesis.
+accumulate HB/common/log.
+
 % This type is private, build it via the APIs below
 typeabbrev phant-term phant.private.phant-term.
 
@@ -257,6 +261,7 @@ mk-phant-term.mixins Target Src CN PF Params N Ty MLwA Out :- std.do! [
   fun-implicit Nlocal Ty Body Out
 ].
 
+func mk-phant-term.mixins.aux term, list term, term, gref, phant-term -> phant-term.
 mk-phant-term.mixins.aux T Params C CN PF X :- std.do![
   get-constructor CN KC,
   synthesis.infer-all-gref->deps Params T KC KCM,
diff --git a/HB/common/synthesis.elpi b/HB/common/synthesis.elpi
index 8a0b5752..2d23c3f1 100644
--- a/HB/common/synthesis.elpi
+++ b/HB/common/synthesis.elpi
@@ -11,6 +11,8 @@
 % a bunch of mixins at hand and does want to pass them down to other terms,
 % without explictly saying exactly where they should be used.
 
+accumulate HB/common/database.
+
 namespace synthesis {
 
 % [infer-all-these-mixin-args Ps T ML F X] fills in all the arguments of F
diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi
index 07d859b3..cbcab49c 100644
--- a/HB/common/utils.elpi
+++ b/HB/common/utils.elpi
@@ -3,7 +3,8 @@
 
 
 % This file contains some HB specific utilities
-accumulate HB/common/utils-synterp.
+accumulate HB/common/utils_synterp.
+accumulate HB/common/stdpp.
 
 shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }.
 
@@ -26,11 +27,9 @@ with-locality P :-
 func acc-clause scope, prop.
 acc-clause Scope C :- coq.elpi.accumulate Scope "hb.db" (clause _ _ C).
 
-/* Uncomment and remove HB/common/compat_acc_clauses_*.elpi once requiring coq-elpi >= 1.18.0,
-   which implies Coq >= 8.17
-pred acc-clauses i:scope, i:list prop.
+:index (1)
+func acc-clauses scope, list prop.
 acc-clauses Scope CL :- coq.elpi.accumulate-clauses Scope "hb.db" {std.map CL (c\r\ r = clause _ _ c)}.
-*/
 
 % TODO: Should this only be used for gref that are factories? (and check in the first/second branch so?)
 % Should we make this an HO predicate, eg "located->gref S L is-factory? GR"
diff --git a/HB/common/utils-synterp.elpi b/HB/common/utils_synterp.elpi
similarity index 100%
rename from HB/common/utils-synterp.elpi
rename to HB/common/utils_synterp.elpi
diff --git a/HB/context.elpi b/HB/context.elpi
index 28c917d0..a4d5427d 100644
--- a/HB/context.elpi
+++ b/HB/context.elpi
@@ -1,6 +1,9 @@
 /*        Hierarchy Builder: algebraic hierarchies made easy
     This software is released under the terms of the MIT license              */
 
+accumulate HB/common/log.
+accumulate HB/instance.
+
 namespace context {
 
 pred declare i:factories, o:mixins, o:list term, o:term, o:list prop, o:list constant.
diff --git a/HB/export.elpi b/HB/export.elpi
index fc66845b..1227ad9e 100644
--- a/HB/export.elpi
+++ b/HB/export.elpi
@@ -1,6 +1,9 @@
 /*        Hierarchy Builder: algebraic hierarchies made easy
     This software is released under the terms of the MIT license              */
 
+accumulate HB/common/database.
+accumulate HB/common/log.
+
 func export.any id ->.
 export.any S :-
   coq.locate-all S L,
diff --git a/HB/factory.elpi b/HB/factory.elpi
index cd8794b9..9dc4da30 100644
--- a/HB/factory.elpi
+++ b/HB/factory.elpi
@@ -1,6 +1,13 @@
 /*        Hierarchy Builder: algebraic hierarchies made easy
     This software is released under the terms of the MIT license              */
 
+accumulate HB/common/database.
+accumulate HB/common/log.
+accumulate HB/common/synthesis.
+accumulate HB/common/phant-abbreviation.
+accumulate HB/context.
+accumulate HB/export.
+
 namespace factory {
 
 func declare argument ->.
@@ -198,6 +205,7 @@ declare-id-builder GR (from GR GR (const C)) :- std.do! [
   std.assert-ok! (coq.elaborate-skeleton IDBodySkel IDType IDBody) "identity builder illtyped",
   log.coq.env.add-const-noimplicits "identity_builder" IDBody IDType @transparent! C,
 ].
+func declare-id-builder.aux gref, list term, term -> term.
 declare-id-builder.aux GR Params TheType (fun `x` Ty x\x) :-
   synthesis.infer-all-gref->deps Params TheType GR Ty.
 
diff --git a/HB/graph.elpi b/HB/graph.elpi
index ead73a8b..a027cddc 100644
--- a/HB/graph.elpi
+++ b/HB/graph.elpi
@@ -1,6 +1,9 @@
 /*        Hierarchy Builder: algebraic hierarchies made easy
     This software is released under the terms of the MIT license              */
 
+accumulate HB/common/database.
+accumulate HB/common/log.
+
 namespace graph {
 
 func to-file string ->.
diff --git a/HB/howto.elpi b/HB/howto.elpi
index 2ca7916e..7ade653c 100644
--- a/HB/howto.elpi
+++ b/HB/howto.elpi
@@ -1,6 +1,9 @@
 /*        Hierarchy Builder: algebraic hierarchies made easy
     This software is released under the terms of the MIT license              */
 
+accumulate HB/common/database.
+accumulate HB/about.
+
 namespace howto {
 
 :index (1)
diff --git a/HB/instance.elpi b/HB/instance.elpi
index f7f6eb1a..708c2052 100644
--- a/HB/instance.elpi
+++ b/HB/instance.elpi
@@ -1,6 +1,9 @@
 /*        Hierarchy Builder: algebraic hierarchies made easy
     This software is released under the terms of the MIT license              */
 
+accumulate HB/common/log.
+accumulate HB/common/synthesis.
+
 namespace instance {
 
 % [declare-existing T F] equips T with all the canonical structures that can be
diff --git a/HB/pack.elpi b/HB/pack.elpi
index 3bd0d2cc..0f8ebc93 100644
--- a/HB/pack.elpi
+++ b/HB/pack.elpi
@@ -2,6 +2,10 @@
 /*        Hierarchy Builder: algebraic hierarchies made easy
     This software is released under the terms of the MIT license              */
 
+accumulate HB/common/database.
+accumulate HB/common/synthesis.
+accumulate HB/common/log.
+
 namespace pack {
 
 pred main i:term, i:list argument, o:term.
diff --git a/HB/status.elpi b/HB/status.elpi
index e6bf3684..7a44e68b 100644
--- a/HB/status.elpi
+++ b/HB/status.elpi
@@ -1,6 +1,8 @@
 /*        Hierarchy Builder: algebraic hierarchies made easy
     This software is released under the terms of the MIT license              */
 
+accumulate HB/common/database.
+
 namespace status {
 
 pred print-hierarchy.
diff --git a/HB/structure.elpi b/HB/structure.elpi
index 52036dfd..86e97047 100644
--- a/HB/structure.elpi
+++ b/HB/structure.elpi
@@ -1,6 +1,12 @@
 /*        Hierarchy Builder: algebraic hierarchies made easy
     This software is released under the terms of the MIT license              */
 
+accumulate HB/common/database.
+accumulate HB/common/phant-abbreviation.
+accumulate HB/common/log.
+accumulate HB/factory.
+accumulate HB/instance.
+
 namespace structure {
 
 % HB.structure Definition S P1 P2 := { T of F1 P1 T & F2 P1 (P2*P2) T }
diff --git a/HB/structures.v b/HB/structures.v
index 90fcb358..0c3c7b61 100644
--- a/HB/structures.v
+++ b/HB/structures.v
@@ -62,198 +62,7 @@ Global Open Scope HB_scope.
 (** This data represents the hierarchy and some other piece of state to
     implement the commands of this file *)
 
-#[interp] Elpi Db hb.db lp:{{
-
-typeabbrev mixinname   gref.
-typeabbrev classname   gref.
-typeabbrev factoryname gref.
-typeabbrev structure   gref.
-
-typeabbrev (w-args A) (triple A (list term) term).
-
-kind w-params type -> type.
-type w-params.cons id -> term -> (term -> w-params A) -> w-params A.
-type w-params.nil id -> term -> (term -> A) -> w-params A.
-
-typeabbrev (list-w-params A) (w-params (list (w-args A))).
-typeabbrev (one-w-params A) (w-params (w-args A)).
-typeabbrev mixins (list-w-params mixinname).
-typeabbrev factories (list-w-params mixinname).
-typeabbrev (w-mixins A) (pair mixins (w-params A)).
-
-%%%%% Classes %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-% (class C S ML) represents a class C packed in S containing mixins ML.
-% Example:
-%
-%  HB.mixin Record IsZmodule V := { ... }
-%  HB.mixin Record Zmodule_IsLmodule (R : ringType) V of Zmodule V := { ... }
-%  HB.structure Definition Lmodule R := {M of Zmodule M & Zmodule_IsLmodule R M}
-%
-% The class description for Lmodule would be:
-%
-%  class (indt «Lmodule.axioms»)                   /* The record with all mixins     */
-%        (indt «Lmodule.type»)                     /* The record with sort and class */
-%        (w-params.cons "R" {{ Ring.type }} P \    /* The first parameter, named "R" */
-%          w-params.nil "M" {{ Type }} T \         /* The key of the structure       */
-%           [...,                                  /* deps of IsZmodule.mixin        */
-%            triple (indt «IsZmodule.mixin») [] T, /* a mixins with its params       */
-%            triple (indt «Zmodule_IsLmodule.mixin») [P] T ]) /* another mixins      */
-%
-% If some mixin parameters depend on other mixins (through a canonical instance that
-% can be inferred from them). Since our structure does not account for dependencies
-% between mixins (the list in the end is flat), we compensate by replacing canonical
-% instances by calls to `S.Pack T {{lib:elpi.hole}}`, and extending the reconstruction
-% mecanism of mixins to also reinfer these holes.
-
-kind hbclass type.
-type class classname -> structure -> mixins -> hbclass.
-
-% class-def contains all the classes ever declared
-pred class-def o:hbclass.
-
-%%%%% Builders %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-% [from FN MN F] invariant:
-% "F : forall p1 .. pn T LMN, FN p1 .. pn T LMN1 -> MN c1 .. cm T LMN2" where
-%  - LMN1 and LMN2 are sub lists of LMN
-%  - c1 .. cm are terms built using p1 .. pn and T
-% - [factory-requires FN LMN]
-% [from _ M _] tests whether M is a declared mixin.
-pred from o:factoryname, o:mixinname, o:gref.
-
-%%%%% Abbreviations %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-% [phant-abbrev Cst AbbrevCst Abbrev]
-% Stores phantom abbreviation Abbrev associated with Cst
-% AbbrevCst is the constant that serves as support
-% e.g. Definition AbbrevCst := fun t1 t2 (phant_id t1 t2) => Cst t2.
-%      Notation   Abbrev t1 := (AbbrevCst t1 _ idfun).
-pred phant-abbrev o:gref, o:gref, o:abbreviation.
-
-% [factory-alias->gref X GR] when X is already a factory X = GR
-% however, when X is a phantom abbreviated gref, we find the underlying
-% factory gref GR associated to it.
-func factory-alias->gref gref -> gref, diagnostic.
-factory-alias->gref PhGR GR ok :- phant-abbrev GR PhGR _, !.
-factory-alias->gref GR GR ok :- phant-abbrev GR _ _, !.
-factory-alias->gref GR _ (error Msg) :- !,
-  Msg is {coq.term->string (global GR)} ^
-         " is not a factory or its library (" ^
-        { std.string.concat "." {std.drop-last 1 {coq.gref->path GR} } } ^
-        ") was not correctly imported".
-
-%%%%% Cache of known facts %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-% [factory->constructor F K] means K is a constructor for
-% the factory F.
-:index(2)
-func factory->constructor factoryname -> gref.
-
-% [factory->nparams F N] says that F has N parameters
-:index(2)
-func factory->nparams factoryname -> int.
-
-% [is-structure GR] tests if GR is a known structure
-pred is-structure o:gref.
-
-% [is-factory GR] tests if GR is a known factory
-pred is-factory o:gref.
-
-% [sub-class C1 C2 Coercion12 NparamsCoercion] C1 is a sub-class of C2,
-% see also sub-class? which computes it on the fly
-:index (2 2 1)
-pred sub-class o:classname, o:classname, o:constant, o:int.
-
-% [gref->deps GR MLwP] is a (pre computed) list of dependencies of a know global
-% constant. The list is topologically sorted
-:index(2)
-func gref->deps gref -> mixins.
-
-% [join C1 C2 C3] means that C3 inherits from both C1 and C2
-pred join o:classname, o:classname, o:classname.
-
-% Section local memory of names for mixins, so that we can reuse them
-% and build terms with simpler conversion problems (less unfolding
-% in order to discover two mixins are the same)
-% @gares : is it really a func. Ideally I think so, bu we load mixin-mem via
-% `Clauses =>` in infer-class. Should perform a dynamic check?
-func mixin-mem term -> gref.
-
-%%%%%% Memory of exported mixins (HB.structure) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Operations (named mixin fields) need to be exported exactly once,
-% but the same mixin can be used in many structure, hence this memory
-% to keep the invariant.
-% Also we remember which is the first class/structure that includes
-% a given mixin, assuming the invariant that this first class is also
-% the minimal class that includes this mixin.
-% [mixin->first-class M C] states that C is the first/minimal class
-% that contains the mixin M
-:index(2)
-func mixin->first-class mixinname -> classname.
-
-% memory of exported operations (TODO: document fiels)
-pred exported-op o:mixinname, o:constant, o:constant.
-
-% memory of factory sort coercion
-pred factory-sort o:coercion.
-
-% memory of canonical projections for a structure (X.sort, X.class, X.type)
-pred structure-key o:constant, o:constant, o:structure.
-
-%%%%%% Membership of mixins to a  class %%%%%%%%%%%%%%%%
-% [mixin-class M C] means M belongs to C
-pred mixin-class o:mixinname, o:classname.
-
-%% database for HB.context %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-% [mixin-src T M X] states that X can be used to reconstruct
-% an instance of the mixin [M T …], directly or through a builder.
-% Since HB.builders sections can declare canonical instances of
-% mixins that do not yet form a structure, we cannot resort to
-% Coq's CS database (which is just for structures).
-pred mixin-src o:term, o:mixinname, o:term.
-
-% [has-mixin-instance K M G] states that G is a reference to an instance
-% of mixin M for subject K
-pred has-mixin-instance o:cs-pattern, o:mixinname, o:gref.
-
-%% database for HB.builders %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-% [builder N TheFactory TheMixin S] is used to
-% remember that the user run [HB.instance S] hence [HB.end] has to
-% synthesize builders from TheFactory to TheMixin mixins generated by S.
-% N is a timestamp.
-kind builder type.
-type builder int -> factoryname -> mixinname -> gref -> builder.
-pred builder-decl o:builder.
-
-%% database for builder-local canonical instances %%%%%%%%%%%%%%%%%%%%%%%
-pred local-canonical o:constant.
-
-% To tell HB.end what we are doing
-kind declaration type.
-% TheType, TheFactory and it's name and the name of the module encloding all that
-type builder-from term -> term -> factoryname -> id -> declaration.
-type no-builder declaration.
-pred current-mode o:declaration.
-
-%% database for HB.export / HB.reexport %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-% library, nice-name, object
-pred module-to-export   o:string, o:id, o:modpath.
-pred instance-to-export o:string, o:id, o:constant.
-pred abbrev-to-export   o:string, o:id, o:gref.
-pred clause-to-export   o:string, o:prop.
-
-%% database for HB.locate and HB.about %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-pred decl-location o:gref, o:loc.
-
-% [docstring Loc Doc] links a location in the source text and some doc
-pred docstring o:loc, o:string.
-
-}}.
+#[interp] Elpi Db hb.db lp:{{ accumulate HB/common/database_signature. }}.
 
 (* This database is used by the parsing phase only *)
 #[synterp] Elpi Db export.db lp:{{
@@ -262,6 +71,27 @@ pred docstring o:loc, o:string.
 }}.
 
 
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+
+
+From HB.common Extra Dependency "utils_synterp.elpi" as utils_synterp.
+From HB.common Extra Dependency "database.elpi" as database.
+From HB Extra Dependency "about.elpi" as about.
+From HB Extra Dependency "builders.elpi" as builders.
+From HB Extra Dependency "context.elpi" as context.
+From HB Extra Dependency "export.elpi" as export.
+From HB Extra Dependency "factory.elpi" as factory.
+From HB Extra Dependency "graph.elpi" as graph.
+From HB Extra Dependency "howto.elpi" as howto.
+From HB Extra Dependency "instance.elpi" as instance.
+From HB Extra Dependency "pack.elpi" as pack.
+From HB Extra Dependency "status.elpi" as status.
+From HB Extra Dependency "structure.elpi" as structure.
+From HB Extra Dependency "check.elpi" as check.
+
+
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -271,12 +101,7 @@ pred docstring o:loc, o:string.
 *)
 
 #[arguments(raw)] Elpi Command HB.locate.
-Elpi Accumulate Db hb.db.
-(* Since it can become rather large, accumulating the DB is often by far the
-   most expensive accumulation. It is then worth sharing its cache between
-   the commands. To this end, we accumulate the DB first in each command to
-   ensure the same dependencies and maximize cache hits. For instance, this
-   can save a few (2 or 3) percents of total compilation time on MathComp. *)
+Elpi Accumulate File database.
 Elpi Accumulate lp:{{
 
 :name "start"
@@ -287,7 +112,7 @@ main [str S] :- !,
 
 main _ :- coq.error "Usage: HB.locate <name>.".
 }}.
-Elpi Typecheck.
+Elpi Accumulate Db hb.db.
 Elpi Export HB.locate.
 
 
@@ -305,14 +130,7 @@ Elpi Export HB.locate.
 *)
 
 #[arguments(raw)] Elpi Command HB.about.
-Elpi Accumulate Db hb.db.
-Elpi Accumulate File "HB/common/stdpp.elpi".
-Elpi Accumulate File "HB/common/utils.elpi".
-Elpi Accumulate File "HB/common/database.elpi".
-Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
-Elpi Accumulate File "HB/common/log.elpi".
-Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
-Elpi Accumulate File "HB/about.elpi".
+Elpi Accumulate File about.
 Elpi Accumulate lp:{{
 
 :name "start"
@@ -320,7 +138,7 @@ main [str S] :- !, with-attributes (with-logging (about.main S)).
 
 main _ :- coq.error "Usage: HB.about <name>.".
 }}.
-Elpi Typecheck.
+Elpi Accumulate Db hb.db.
 Elpi Export HB.about.
 
 
@@ -339,15 +157,7 @@ Elpi Export HB.about.
 *)
 
 #[arguments(raw)] Elpi Command HB.howto.
-Elpi Accumulate Db hb.db.
-Elpi Accumulate File "HB/common/stdpp.elpi".
-Elpi Accumulate File "HB/common/database.elpi".
-Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
-Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
-Elpi Accumulate File "HB/common/utils.elpi".
-Elpi Accumulate File "HB/common/log.elpi".
-Elpi Accumulate File "HB/about.elpi".
-Elpi Accumulate File "HB/howto.elpi".
+Elpi Accumulate File howto.
 Elpi Accumulate lp:{{
 
 :name "start"
@@ -368,7 +178,7 @@ main _ :-
   coq.error
     "Usage: HB.howto [(<type>)|<structure>] <structure> [<search depth>].".
 }}.
-Elpi Typecheck.
+Elpi Accumulate Db hb.db.
 Elpi Export HB.howto.
 
 
@@ -381,14 +191,7 @@ Elpi Export HB.howto.
 *)
 
 #[arguments(raw)] Elpi Command HB.status.
-Elpi Accumulate Db hb.db.
-Elpi Accumulate File "HB/common/stdpp.elpi".
-Elpi Accumulate File "HB/common/database.elpi".
-Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
-Elpi Accumulate File "HB/common/log.elpi".
-Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
-Elpi Accumulate File "HB/common/utils.elpi".
-Elpi Accumulate File "HB/status.elpi".
+Elpi Accumulate File status.
 Elpi Accumulate lp:{{
 
 :name "start"
@@ -396,7 +199,7 @@ main [] :- !, status.print-hierarchy.
 
 main _ :- coq.error "Usage: HB.status.".
 }}.
-Elpi Typecheck.
+Elpi Accumulate Db hb.db.
 Elpi Export HB.status.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -411,14 +214,7 @@ tred file.dot | xdot -
 *)
 
 #[arguments(raw)] Elpi Command HB.graph.
-Elpi Accumulate Db hb.db.
-Elpi Accumulate File "HB/common/stdpp.elpi".
-Elpi Accumulate File "HB/common/database.elpi".
-Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
-Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
-Elpi Accumulate File "HB/common/utils.elpi".
-Elpi Accumulate File "HB/common/log.elpi".
-Elpi Accumulate File "HB/graph.elpi".
+Elpi Accumulate File graph.
 Elpi Accumulate lp:{{
 
 :name "start"
@@ -426,7 +222,7 @@ main [str File] :- with-attributes (with-logging (graph.to-file File)).
 main _ :- coq.error "Usage: HB.graph <filename>.".
 
 }}.
-Elpi Typecheck.
+Elpi Accumulate Db hb.db.
 Elpi Export HB.graph.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -460,27 +256,17 @@ HB.mixin Record MixinName T & Factory1 T & … & FactoryN T := {
 *)
 
 #[arguments(raw)] Elpi Command HB.mixin.
-Elpi Accumulate Db hb.db.
-Elpi Accumulate File "HB/common/stdpp.elpi".
-Elpi Accumulate File "HB/common/database.elpi".
-Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
-Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
-Elpi Accumulate File "HB/common/utils.elpi".
-Elpi Accumulate File "HB/common/log.elpi".
-Elpi Accumulate File "HB/common/synthesis.elpi".
-Elpi Accumulate File "HB/common/phant-abbreviation.elpi".
-Elpi Accumulate File "HB/instance.elpi".
-Elpi Accumulate File "HB/context.elpi".
-Elpi Accumulate File "HB/export.elpi".
-Elpi Accumulate File "HB/factory.elpi".
+Elpi Accumulate File factory.
 Elpi Accumulate lp:{{
 
 :name "start"
 main [A] :- with-attributes (with-logging (factory.declare-mixin A)).
 
 }}.
-#[synterp] Elpi Accumulate File "HB/common/utils-synterp.elpi".
-#[synterp] Elpi Accumulate Db export.db.
+Elpi Accumulate Db hb.db.
+
+#[synterp] Elpi Accumulate Db Header export.db.
+#[synterp] Elpi Accumulate File utils_synterp.
 #[synterp] Elpi Accumulate lp:{{
 
 shorten coq.env.{ begin-module, end-module, begin-section, end-section, export-module }.
@@ -502,7 +288,7 @@ main [indt-decl D] :- record-decl->id D N, with-attributes (actions N).
 main _ :-
   coq.error "Usage: HB.mixin Record <MixinName> T & F A & … := { … }.".
 }}.
-Elpi Typecheck.
+#[synterp] Elpi Accumulate Db export.db.
 Elpi Export HB.mixin.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -542,15 +328,7 @@ Elpi Export HB.mixin.
 *)
 
 Elpi Tactic HB.pack_for.
-Elpi Accumulate Db hb.db.
-Elpi Accumulate File "HB/common/stdpp.elpi".
-Elpi Accumulate File "HB/common/database.elpi".
-Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
-Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
-Elpi Accumulate File "HB/common/utils.elpi".
-Elpi Accumulate File "HB/common/log.elpi".
-Elpi Accumulate File "HB/common/synthesis.elpi".
-Elpi Accumulate File "HB/pack.elpi".
+Elpi Accumulate File pack.
 Elpi Accumulate lp:{{
 
 :name "start"
@@ -561,19 +339,11 @@ solve (goal _ _ S _ [trm Ty | Args] as G) GLS :- with-attributes (with-logging (
 ])).
 
 }}.
-Elpi Typecheck.
+Elpi Accumulate Db hb.db.
 Elpi Export HB.pack_for.
 
 Elpi Tactic HB.pack.
-Elpi Accumulate Db hb.db.
-Elpi Accumulate File "HB/common/stdpp.elpi".
-Elpi Accumulate File "HB/common/database.elpi".
-Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
-Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
-Elpi Accumulate File "HB/common/utils.elpi".
-Elpi Accumulate File "HB/common/log.elpi".
-Elpi Accumulate File "HB/common/synthesis.elpi".
-Elpi Accumulate File "HB/pack.elpi".
+Elpi Accumulate File pack.
 Elpi Accumulate lp:{{
 
 :name "start"
@@ -584,7 +354,7 @@ solve (goal _ _ Ty _ Args as G) GLS :- with-attributes (with-logging (std.do! [
 ])).
 
 }}.
-Elpi Typecheck.
+Elpi Accumulate Db hb.db.
 Elpi Export HB.pack.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -641,20 +411,7 @@ HB.structure Definition StructureName params :=
 *)
 
 #[arguments(raw)] Elpi Command HB.structure.
-Elpi Accumulate Db hb.db.
-Elpi Accumulate File "HB/common/stdpp.elpi".
-Elpi Accumulate File "HB/common/database.elpi".
-Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
-Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
-Elpi Accumulate File "HB/common/utils.elpi".
-Elpi Accumulate File "HB/common/log.elpi".
-Elpi Accumulate File "HB/common/synthesis.elpi".
-Elpi Accumulate File "HB/common/phant-abbreviation.elpi".
-Elpi Accumulate File "HB/export.elpi".
-Elpi Accumulate File "HB/instance.elpi".
-Elpi Accumulate File "HB/context.elpi".
-Elpi Accumulate File "HB/factory.elpi".
-Elpi Accumulate File "HB/structure.elpi".
+Elpi Accumulate File structure.
 Elpi Accumulate lp:{{
 
 :name "start"
@@ -666,8 +423,10 @@ main [const-decl N (some B) Arity] :- std.do! [
 ].
 
 }}.
-#[synterp] Elpi Accumulate File "HB/common/utils-synterp.elpi".
-#[synterp] Elpi Accumulate Db export.db.
+Elpi Accumulate Db hb.db.
+
+#[synterp] Elpi Accumulate Db Header export.db.
+#[synterp] Elpi Accumulate File utils_synterp.
 #[synterp] Elpi Accumulate lp:{{
 
 shorten coq.env.{ begin-module, end-module, begin-section, end-section, import-module, export-module }.
@@ -705,7 +464,7 @@ main [const-decl N _ _] :- !, with-attributes (actions N).
 
 main _ :- coq.error "Usage: HB.structure Definition <ModuleName> := { A of <Factory1> A & … & <FactoryN> A }".
 }}.
-Elpi Typecheck.
+#[synterp] Elpi Accumulate Db export.db.
 Elpi Export HB.structure.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -724,19 +483,7 @@ Elpi Export HB.structure.
 *)
 
 #[arguments(raw)] Elpi Command HB.saturate.
-Elpi Accumulate Db hb.db.
-Elpi Accumulate File "HB/common/stdpp.elpi".
-Elpi Accumulate File "HB/common/database.elpi".
-Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
-Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
-Elpi Accumulate File "HB/common/utils.elpi".
-Elpi Accumulate File "HB/common/log.elpi".
-Elpi Accumulate File "HB/common/synthesis.elpi".
-Elpi Accumulate File "HB/common/phant-abbreviation.elpi".
-Elpi Accumulate File "HB/export.elpi".
-Elpi Accumulate File "HB/instance.elpi".
-Elpi Accumulate File "HB/context.elpi".
-Elpi Accumulate File "HB/factory.elpi".
+Elpi Accumulate File factory.
 Elpi Accumulate lp:{{
 main [] :- !, with-attributes (with-logging (instance.saturate-instances _)).
 main [str "Type"] :- !, with-attributes (with-logging (instance.saturate-instances (cs-sort _))).
@@ -744,7 +491,7 @@ main [str K] :- !, coq.locate K GR, with-attributes (with-logging (instance.satu
 main [trm T] :- !, term->cs-pattern T P, with-attributes (with-logging (instance.saturate-instances P)).
 main _ :- coq.error "Usage: HB.saturate [key]".
 }}.
-Elpi Typecheck.
+Elpi Accumulate Db hb.db.
 Elpi Export HB.saturate.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -774,16 +521,7 @@ HB.instance Definition N Params := Factory.Build Params T …
 *)
 
 #[arguments(raw)] Elpi Command HB.instance.
-Elpi Accumulate Db hb.db.
-Elpi Accumulate File "HB/common/stdpp.elpi".
-Elpi Accumulate File "HB/common/database.elpi".
-Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
-Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
-Elpi Accumulate File "HB/common/utils.elpi".
-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".
+Elpi Accumulate File instance.
 Elpi Accumulate lp:{{
 
 :name "start"
@@ -794,6 +532,8 @@ main [T0, F0] :- !,
   with-attributes (with-logging (instance.declare-existing T0 F0)).
 
 }}.
+Elpi Accumulate Db hb.db.
+
 #[synterp] Elpi Accumulate lp:{{
 
 shorten coq.env.{ begin-section, end-section }.
@@ -806,7 +546,6 @@ main [_, _] :- !.
 
 main _ :- coq.error "Usage: HB.instance Definition <Name> := <Builder> T ...".
 }}.
-Elpi Typecheck.
 Elpi Export HB.instance.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -816,26 +555,16 @@ Elpi Export HB.instance.
 (** [HB.factory] declares a factory. It has the same syntax of [HB.mixin] *)
 
 #[arguments(raw)] Elpi Command HB.factory.
-Elpi Accumulate Db hb.db.
-Elpi Accumulate File "HB/common/stdpp.elpi".
-Elpi Accumulate File "HB/common/database.elpi".
-Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
-Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
-Elpi Accumulate File "HB/common/utils.elpi".
-Elpi Accumulate File "HB/common/log.elpi".
-Elpi Accumulate File "HB/common/synthesis.elpi".
-Elpi Accumulate File "HB/common/phant-abbreviation.elpi".
-Elpi Accumulate File "HB/instance.elpi".
-Elpi Accumulate File "HB/context.elpi".
-Elpi Accumulate File "HB/export.elpi".
-Elpi Accumulate File "HB/factory.elpi".
+Elpi Accumulate File factory.
 Elpi Accumulate lp:{{
 
 :name "start"
 main [A] :- with-attributes (with-logging (factory.declare A)).
 
 }}.
-#[synterp] Elpi Accumulate File "HB/common/utils-synterp.elpi".
+Elpi Accumulate Db hb.db.
+
+#[synterp] Elpi Accumulate File utils_synterp.
 #[synterp] Elpi Accumulate Db export.db.
 #[synterp] Elpi Accumulate lp:{{
 
@@ -859,7 +588,6 @@ main [const-decl N _ _] :- with-attributes (actions N).
 main _ :-
   coq.error "Usage: HB.factory Record <FactoryName> T & F A & … := { … }.\nUsage: HB.factory Definition <FactoryName> T of F A := t.".
 }}.
-Elpi Typecheck.
 Elpi Export HB.factory.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -899,27 +627,16 @@ HB.end.
 *)
 
 #[arguments(raw)] Elpi Command HB.builders.
-Elpi Accumulate Db hb.db.
-Elpi Accumulate File "HB/common/stdpp.elpi".
-Elpi Accumulate File "HB/common/database.elpi".
-Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
-Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
-Elpi Accumulate File "HB/common/utils.elpi".
-Elpi Accumulate File "HB/common/log.elpi".
-Elpi Accumulate File "HB/common/synthesis.elpi".
-Elpi Accumulate File "HB/common/phant-abbreviation.elpi".
-Elpi Accumulate File "HB/instance.elpi".
-Elpi Accumulate File "HB/context.elpi".
-Elpi Accumulate File "HB/export.elpi".
-Elpi Accumulate File "HB/factory.elpi".
-Elpi Accumulate File "HB/builders.elpi".
+Elpi Accumulate File builders.
 Elpi Accumulate lp:{{
 
 :name "start"
 main [ctx-decl C] :- with-attributes (with-logging (builders.begin C)).
 
 }}.
-#[synterp] Elpi Accumulate File "HB/common/utils-synterp.elpi".
+Elpi Accumulate Db hb.db.
+
+#[synterp] Elpi Accumulate File utils_synterp.
 #[synterp] Elpi Accumulate lp:{{
 
 shorten coq.env.{ begin-module, end-module, begin-section }.
@@ -935,30 +652,20 @@ main [ctx-decl _] :- !, with-attributes (actions {calc ("Builders_" ^ {std.any->
 
 main _ :- coq.error "Usage: HB.builders Context A (f : F1 A).".
 }}.
-Elpi Typecheck.
 Elpi Export HB.builders.
 
 
 #[arguments(raw)] Elpi Command HB.end.
-Elpi Accumulate Db hb.db.
-Elpi Accumulate File "HB/common/stdpp.elpi".
-Elpi Accumulate File "HB/common/database.elpi".
-Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
-Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
-Elpi Accumulate File "HB/common/utils.elpi".
-Elpi Accumulate File "HB/common/log.elpi".
-Elpi Accumulate File "HB/common/synthesis.elpi".
-Elpi Accumulate File "HB/instance.elpi".
-Elpi Accumulate File "HB/context.elpi".
-Elpi Accumulate File "HB/export.elpi".
-Elpi Accumulate File "HB/builders.elpi".
+Elpi Accumulate File builders.
 Elpi Accumulate lp:{{
 
 :name "start"
 main [] :- with-attributes (with-logging builders.end).
 
 }}.
-#[synterp] Elpi Accumulate File "HB/common/utils-synterp.elpi".
+Elpi Accumulate Db hb.db.
+
+#[synterp] Elpi Accumulate File utils_synterp.
 #[synterp] Elpi Accumulate Db export.db.
 #[synterp] Elpi Accumulate lp:{{
 
@@ -978,7 +685,6 @@ main [] :- !, with-attributes actions.
 main _ :- coq.error "Usage: HB.end.".
 
 }}.
-Elpi Typecheck.
 Elpi Export HB.end.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -1015,12 +721,6 @@ Export Algebra.Exports.
 
 #[arguments(raw)] Elpi Command HB.export.
 Elpi Accumulate Db hb.db.
-Elpi Accumulate File "HB/common/stdpp.elpi".
-Elpi Accumulate File "HB/common/database.elpi".
-Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
-Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
-Elpi Accumulate File "HB/common/utils.elpi".
-Elpi Accumulate File "HB/common/log.elpi".
 Elpi Accumulate File "HB/export.elpi".
 Elpi Accumulate lp:{{
 
@@ -1029,7 +729,7 @@ main [str M] :- !, with-attributes (with-logging (export.any M)).
 main _ :- coq.error "Usage: HB.export M.".
 
 }}.
-#[synterp] Elpi Accumulate File "HB/common/utils-synterp.elpi".
+#[synterp] Elpi Accumulate File utils_synterp.
 #[synterp] Elpi Accumulate Db export.db.
 #[synterp] Elpi Accumulate lp:{{
 
@@ -1046,7 +746,6 @@ main [str M] :- !, with-attributes (actions {coq.locate-all M}).
 main _ :- coq.error "Usage: HB.export M.".
 
 }}.
-Elpi Typecheck.
 Elpi Export HB.export.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -1061,12 +760,6 @@ Elpi Export HB.export.
 
 #[arguments(raw)] Elpi Command HB.reexport.
 Elpi Accumulate Db hb.db.
-Elpi Accumulate File "HB/common/stdpp.elpi".
-Elpi Accumulate File "HB/common/database.elpi".
-Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
-Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
-Elpi Accumulate File "HB/common/utils.elpi".
-Elpi Accumulate File "HB/common/log.elpi".
 Elpi Accumulate File "HB/export.elpi".
 Elpi Accumulate lp:{{
 
@@ -1076,7 +769,7 @@ main [str M] :- !, with-attributes (with-logging (export.reexport-all-modules-an
 main _ :- coq.error "Usage: HB.reexport.".
 
 }}.
-#[synterp] Elpi Accumulate File "HB/common/utils-synterp.elpi".
+#[synterp] Elpi Accumulate File utils_synterp.
 #[synterp] Elpi Accumulate Db export.db.
 #[synterp] Elpi Accumulate lp:{{
 
@@ -1100,7 +793,6 @@ main [str M] :- !, with-attributes (actions (some M)).
 main _ :- coq.error "Usage: HB.reexport.".
 
 }}.
-Elpi Typecheck.
 Elpi Export HB.reexport.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -1144,14 +836,6 @@ HB.instance Definition _ : Ml ... T := ml.
 
 #[arguments(raw)] Elpi Command HB.declare.
 Elpi Accumulate Db hb.db.
-Elpi Accumulate File "HB/common/stdpp.elpi".
-Elpi Accumulate File "HB/common/database.elpi".
-Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
-Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
-Elpi Accumulate File "HB/common/utils.elpi".
-Elpi Accumulate File "HB/common/log.elpi".
-Elpi Accumulate File "HB/common/synthesis.elpi".
-Elpi Accumulate File "HB/common/phant-abbreviation.elpi".
 Elpi Accumulate File "HB/export.elpi".
 Elpi Accumulate File "HB/instance.elpi".
 Elpi Accumulate File "HB/context.elpi".
@@ -1167,7 +851,6 @@ main [Ctx] :- Ctx = ctx-decl _, !,
 main _ :- coq.error "Usage: HB.declare Context <Parameters> <Key> <Factories>".
 
 }}.
-Elpi Typecheck.
 Elpi Export HB.declare.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -1179,35 +862,16 @@ Elpi Export HB.declare.
     [#[fail]] attribute. *)
 
 #[arguments(raw)] Elpi Command HB.check.
-Elpi Accumulate Db hb.db.
-Elpi Accumulate File "HB/common/stdpp.elpi".
-Elpi Accumulate File "HB/common/database.elpi".
-Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
-Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
-Elpi Accumulate File "HB/common/utils.elpi".
-Elpi Accumulate File "HB/common/log.elpi".
+Elpi Accumulate File check.
 Elpi Accumulate lp:{{
 
 :name "start"
 main [trm Skel] :- !, with-attributes (with-logging (check-or-not Skel)).
 main _ :- coq.error "usage: HB.check (term).".
 
-pred check-or-not i:term.
-check-or-not Skel :-
-  coq.version VersionString _ _ _,
-  if (get-option "skip" R, rex_match R VersionString)
-     (coq.warning "HB" "HB.skip" {get-option "elpi.loc"} "Skipping test on Coq" VersionString "as requested")
-     (log.coq.check Skel Ty T Result,
-      if (Result = error Msg)
-         (if (get-option "fail" tt)
-             (coq.say "The command did fail as expected with message:" Msg)
-             (coq.error "HB.check:" Msg))
-         (if (get-option "fail" tt)
-             (coq.error "The command did not fail")
-             (coq.say "HB.check:" {coq.term->string T} ":" {coq.term->string Ty}))).
 
 }}.
-Elpi Typecheck.
+Elpi Accumulate Db hb.db.
 Elpi Export HB.check.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
diff --git a/_CoqProject b/_CoqProject
index d2b6ace7..38bb2b25 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -3,7 +3,7 @@ HB/structures.v
 -arg -w -arg +elpi.typecheck
 -arg -w -arg -elpi.typecheck-syntax
 -arg -w -arg -elpi.flex-clause
--Q HB HB
+-R HB HB
 
 -R tests HB.tests
 -R examples HB.examples