diff --git a/.gitignore b/.gitignore
index 21e65d20f..af8347e06 100644
--- a/.gitignore
+++ b/.gitignore
@@ -34,6 +34,9 @@ nra.cache
 Makefile.coq
 Makefile.coq.conf
 .coqdeps.d
+Makefile.test-suite.coq
+Makefile.test-suite.coq.conf
+.coqdeps.test-suite
 
 _minted-*
 *.aux
diff --git a/Makefile.common b/Makefile.common
index 857ddef27..c51fd521a 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -25,13 +25,13 @@ TGTS?=
 ######################################################################
 
 # local context: -----------------------------------------------------
-.PHONY: all config build only test-suite clean distclean doc doc-clean __always__
+.PHONY: all config build only test-suite clean distclean __always__
 .SUFFIXES:
 
 H:= $(if $(VERBOSE),,@)  # not used yet
 TOP     = $(dir $(lastword $(MAKEFILE_LIST)))
 COQMAKE = $(MAKE) -f Makefile.coq $(COQMAKEOPTIONS)
-COQMAKE_TESTSUITE = $(MAKE) -f Makefile.test-suite.coq VDFILE=".coqdeps.test-suite" $(COQMAKEOPTIONS)
+COQMAKE_TESTSUITE = $(MAKE) -f Makefile.test-suite.coq $(COQMAKEOPTIONS)
 BRANCH_coq:= $(shell $(COQBIN)coqtop -v | head -1 | grep -E '(trunk|master)' \
 	      | wc -l | sed 's/ *//g')
 
@@ -46,7 +46,10 @@ COQV:= $(shell echo $(COQVVV) | cut -d"." -f1)
 COQVV:= $(shell echo $(COQVVV) | cut -d"." -f1-2)
 
 # all: ---------------------------------------------------------------
-all: config build
+all: 
+	$(MAKE) config
+	$(MAKE) build
+	$(MAKE) test-suite
 
 # Makefile.coq: ------------------------------------------------------
 .PHONY: pre-makefile
@@ -56,12 +59,8 @@ Makefile.coq: pre-makefile $(COQPROJECT) Makefile
 
 # Test suite ---------------------------------------------------------
 
-test_suite/hierarchy_test.v: build
-	mkdir -p test_suite
-	COQBIN=$(COQBIN) ocaml ../etc/utils/hierarchy.ml -verify -R . mathcomp -lib all.all > test_suite/hierarchy_test.v
-
-Makefile.test-suite.coq: test_suite/hierarchy_test.v
-	$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f Make.test-suite -o Makefile.test-suite.coq
+Makefile.test-suite.coq: $(COQPROJECT).test-suite Makefile
+	$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f $(COQPROJECT).test-suite -o Makefile.test-suite.coq
 
 # Global config, build, clean and distclean --------------------------
 config: sub-config this-config
@@ -72,7 +71,7 @@ only: sub-only this-only
 
 test-suite: sub-test-suite this-test-suite
 
-clean: sub-clean this-clean doc-clean
+clean: sub-clean this-clean
 
 distclean: sub-distclean this-distclean
 
@@ -125,25 +124,5 @@ sub-%: __always__
 endif
 
 # Make of individual .vo ---------------------------------------------
-%.vo: __always__ Makefile.coq
+structures.vo : %.vo: __always__ Makefile.coq
 	+$(COQMAKE) $@
-
-doc: __always__ Makefile.coq
-	mkdir -p _build_doc/
-	cp -r $(COQFILES) -t _build_doc/ --parents
-	cp Make Makefile* _build_doc
-	mkdir -p _build_doc/htmldoc
-	. ../etc/utils/builddoc_lib.sh; \
-		cd _build_doc && mangle_sources $(COQFILES)
-	+cd _build_doc && $(COQMAKE)
-	cd _build_doc && if [ ! -f .Makefile.coq.d ] ; then cp .coqdeps.d .Makefile.coq.d ; fi #can be removed when coq-8.10 compatibility is dropped
-	cd _build_doc && grep -v vio: .Makefile.coq.d > depend
-	cd _build_doc && cat depend | ../../etc/buildlibgraph $(COQFILES) > htmldoc/depend.js
-	cd _build_doc && $(COQBIN)coqdoc -t "Mathematical Components" \
-		-g --utf8 -R . mathcomp \
-		--parse-comments \
-		--multi-index $(COQFILES) -d htmldoc
-	cp ../etc/artwork/coqdoc.css _build_doc/htmldoc
-
-doc-clean:
-	rm -rf _build_doc/
diff --git a/_CoqProject b/_CoqProject
index 3f60e011f..0d6fc6f3e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,60 +1,4 @@
 structures.v
 
-readme.v
-
-demo1/hierarchy_0.v
-demo1/hierarchy_1.v
-demo1/hierarchy_2.v
-demo1/hierarchy_3.v
-demo1/hierarchy_4.v
-demo1/hierarchy_5.v
-demo1/test_0_0.v
-demo1/test_1_0.v
-demo1/test_2_0.v
-demo1/test_3_0.v
-demo1/test_3_3.v
-demo1/test_4_0.v
-demo1/test_4_3.v
-demo1/test_5_0.v
-demo1/test_5_3.v
-
-demo2/classical.v
-demo2/stage10.v
-demo2/stage11.v
-
-demo3/hierarchy_0.v
-demo3/hierarchy_1.v
-demo3/hierarchy_2.v
-demo3/test_0_0.v
-demo3/test_1_0.v
-demo3/test_2_0.v
-
-demo4/hierarchy_0.v
-
-demo5/hierarchy_0.v
-
-FSCD2020_material/V1.v
-FSCD2020_material/V2.v
-FSCD2020_material/V3.v
-FSCD2020_material/V4.v
-
-FSCD2020_talk/V1.v
-FSCD2020_talk/V2.v
-FSCD2020_talk/V3.v
-
-Coq2020_material/CoqWS_demo.v
-Coq2020_material/CoqWS_abstract.v
-Coq2020_material/CoqWS_expansion/withHB.v
-Coq2020_material/CoqWS_expansion/withoutHB.v
-
-tests/type_of_exported_ops.v
-tests/duplicate_structure.v
-tests/instance_params_no_type.v
-tests/test_CS_db_filtering.v
-tests/subtype.v
-tests/exports.v
-tests/infer.v
-tests/display.v
-
--R . HB
 -arg -w -arg -elpi.add-const-for-axiom-or-sectionvar
+-Q . HB
diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite
new file mode 100644
index 000000000..0d197eea8
--- /dev/null
+++ b/_CoqProject.test-suite
@@ -0,0 +1,60 @@
+examples/readme.v
+
+examples/demo1/hierarchy_0.v
+examples/demo1/hierarchy_1.v
+examples/demo1/hierarchy_2.v
+examples/demo1/hierarchy_3.v
+examples/demo1/hierarchy_4.v
+examples/demo1/hierarchy_5.v
+examples/demo1/test_0_0.v
+examples/demo1/test_1_0.v
+examples/demo1/test_2_0.v
+examples/demo1/test_3_0.v
+examples/demo1/test_3_3.v
+examples/demo1/test_4_0.v
+examples/demo1/test_4_3.v
+examples/demo1/test_5_0.v
+examples/demo1/test_5_3.v
+
+examples/demo2/classical.v
+examples/demo2/stage10.v
+examples/demo2/stage11.v
+
+examples/demo3/hierarchy_0.v
+examples/demo3/hierarchy_1.v
+examples/demo3/hierarchy_2.v
+examples/demo3/test_0_0.v
+examples/demo3/test_1_0.v
+examples/demo3/test_2_0.v
+
+examples/demo4/hierarchy_0.v
+
+examples/demo5/hierarchy_0.v
+
+examples/FSCD2020_material/V1.v
+examples/FSCD2020_material/V2.v
+examples/FSCD2020_material/V3.v
+examples/FSCD2020_material/V4.v
+
+examples/FSCD2020_talk/V1.v
+examples/FSCD2020_talk/V2.v
+examples/FSCD2020_talk/V3.v
+
+examples/Coq2020_material/CoqWS_demo.v
+examples/Coq2020_material/CoqWS_abstract.v
+examples/Coq2020_material/CoqWS_expansion/withHB.v
+examples/Coq2020_material/CoqWS_expansion/withoutHB.v
+
+tests/type_of_exported_ops.v
+tests/duplicate_structure.v
+tests/instance_params_no_type.v
+tests/test_CS_db_filtering.v
+tests/subtype.v
+tests/infer.v
+tests/exports.v
+
+-R tests HB.tests
+-R examples HB.examples
+
+-Q . HB
+-arg -w -arg -elpi.add-const-for-axiom-or-sectionvar
diff --git a/coq-hierarchy-builder.opam b/coq-hierarchy-builder.opam
index 3a31049a3..8de06ee2f 100644
--- a/coq-hierarchy-builder.opam
+++ b/coq-hierarchy-builder.opam
@@ -8,9 +8,11 @@ homepage: "https://github.com/math-comp/hierarchy-builder"
 bug-reports: "https://github.com/math-comp/hierarchy-builder/issues"
 dev-repo: "git+https://github.com/math-comp/hierarchy-builder"
 
-build: [ make ]
-install: [ make "install" "VFILES=structures.v" ]
 depends: [ "coq-elpi" {>= "1.6" & < "1.9~"} ]
+build: [ [ make "build"]
+         [ make "test-suite" ]  # {with-test} waiting https://github.com/coq-community/docker-coq-action/pull/48
+       ]
+install: [ make "install" ]
 synopsis: "High level commands to declare and evolve a hierarchy based on packed classes"
 description: """
 Hierarchy Builder is a high level language to build hierarchies of algebraic structures and make these
diff --git a/Coq2020_material/CoqWS_abstract.v b/examples/Coq2020_material/CoqWS_abstract.v
similarity index 100%
rename from Coq2020_material/CoqWS_abstract.v
rename to examples/Coq2020_material/CoqWS_abstract.v
diff --git a/Coq2020_material/CoqWS_demo.v b/examples/Coq2020_material/CoqWS_demo.v
similarity index 100%
rename from Coq2020_material/CoqWS_demo.v
rename to examples/Coq2020_material/CoqWS_demo.v
diff --git a/Coq2020_material/CoqWS_expansion/withHB.v b/examples/Coq2020_material/CoqWS_expansion/withHB.v
similarity index 100%
rename from Coq2020_material/CoqWS_expansion/withHB.v
rename to examples/Coq2020_material/CoqWS_expansion/withHB.v
diff --git a/Coq2020_material/CoqWS_expansion/withoutHB.v b/examples/Coq2020_material/CoqWS_expansion/withoutHB.v
similarity index 100%
rename from Coq2020_material/CoqWS_expansion/withoutHB.v
rename to examples/Coq2020_material/CoqWS_expansion/withoutHB.v
diff --git a/Coq2020_material/diagram.pdf b/examples/Coq2020_material/diagram.pdf
similarity index 100%
rename from Coq2020_material/diagram.pdf
rename to examples/Coq2020_material/diagram.pdf
diff --git a/Coq2020_material/diagram.svg b/examples/Coq2020_material/diagram.svg
similarity index 100%
rename from Coq2020_material/diagram.svg
rename to examples/Coq2020_material/diagram.svg
diff --git a/FSCD2020_material/V1.v b/examples/FSCD2020_material/V1.v
similarity index 100%
rename from FSCD2020_material/V1.v
rename to examples/FSCD2020_material/V1.v
diff --git a/FSCD2020_material/V2.v b/examples/FSCD2020_material/V2.v
similarity index 100%
rename from FSCD2020_material/V2.v
rename to examples/FSCD2020_material/V2.v
diff --git a/FSCD2020_material/V3.v b/examples/FSCD2020_material/V3.v
similarity index 100%
rename from FSCD2020_material/V3.v
rename to examples/FSCD2020_material/V3.v
diff --git a/FSCD2020_material/V4.v b/examples/FSCD2020_material/V4.v
similarity index 100%
rename from FSCD2020_material/V4.v
rename to examples/FSCD2020_material/V4.v
diff --git a/FSCD2020_talk/V1.v b/examples/FSCD2020_talk/V1.v
similarity index 100%
rename from FSCD2020_talk/V1.v
rename to examples/FSCD2020_talk/V1.v
diff --git a/FSCD2020_talk/V2.v b/examples/FSCD2020_talk/V2.v
similarity index 79%
rename from FSCD2020_talk/V2.v
rename to examples/FSCD2020_talk/V2.v
index 4fb56321a..9c9f5817c 100644
--- a/FSCD2020_talk/V2.v
+++ b/examples/FSCD2020_talk/V2.v
@@ -18,6 +18,6 @@ HB.structure Definition Monoid :=
   { M & monoid_of_semigroup M }.
 
 (* is_monoid does not exist anymore *)
-Fail HB.instance Definition Z_is_monoid : is_monoid Z :=
-  is_monoid.Build Z 0%Z Z.add
-    Z.add_assoc Z.add_0_l Z.add_0_r.
+Fail Check is_monoid.
+
+Fail HB.mixin Record xxxx P A := { F : bool }.
diff --git a/FSCD2020_talk/V3.v b/examples/FSCD2020_talk/V3.v
similarity index 100%
rename from FSCD2020_talk/V3.v
rename to examples/FSCD2020_talk/V3.v
diff --git a/demo1/README.md b/examples/demo1/README.md
similarity index 100%
rename from demo1/README.md
rename to examples/demo1/README.md
diff --git a/demo1/hierarchy_0.v b/examples/demo1/hierarchy_0.v
similarity index 100%
rename from demo1/hierarchy_0.v
rename to examples/demo1/hierarchy_0.v
diff --git a/demo1/hierarchy_1.v b/examples/demo1/hierarchy_1.v
similarity index 100%
rename from demo1/hierarchy_1.v
rename to examples/demo1/hierarchy_1.v
diff --git a/demo1/hierarchy_2.v b/examples/demo1/hierarchy_2.v
similarity index 100%
rename from demo1/hierarchy_2.v
rename to examples/demo1/hierarchy_2.v
diff --git a/demo1/hierarchy_3.v b/examples/demo1/hierarchy_3.v
similarity index 100%
rename from demo1/hierarchy_3.v
rename to examples/demo1/hierarchy_3.v
diff --git a/demo1/hierarchy_4.v b/examples/demo1/hierarchy_4.v
similarity index 100%
rename from demo1/hierarchy_4.v
rename to examples/demo1/hierarchy_4.v
diff --git a/demo1/hierarchy_5.v b/examples/demo1/hierarchy_5.v
similarity index 100%
rename from demo1/hierarchy_5.v
rename to examples/demo1/hierarchy_5.v
diff --git a/demo1/test_0_0.v b/examples/demo1/test_0_0.v
similarity index 100%
rename from demo1/test_0_0.v
rename to examples/demo1/test_0_0.v
diff --git a/demo1/test_1_0.v b/examples/demo1/test_1_0.v
similarity index 100%
rename from demo1/test_1_0.v
rename to examples/demo1/test_1_0.v
diff --git a/demo1/test_2_0.v b/examples/demo1/test_2_0.v
similarity index 100%
rename from demo1/test_2_0.v
rename to examples/demo1/test_2_0.v
diff --git a/demo1/test_3_0.v b/examples/demo1/test_3_0.v
similarity index 100%
rename from demo1/test_3_0.v
rename to examples/demo1/test_3_0.v
diff --git a/demo1/test_3_3.v b/examples/demo1/test_3_3.v
similarity index 100%
rename from demo1/test_3_3.v
rename to examples/demo1/test_3_3.v
diff --git a/demo1/test_4_0.v b/examples/demo1/test_4_0.v
similarity index 100%
rename from demo1/test_4_0.v
rename to examples/demo1/test_4_0.v
diff --git a/demo1/test_4_3.v b/examples/demo1/test_4_3.v
similarity index 100%
rename from demo1/test_4_3.v
rename to examples/demo1/test_4_3.v
diff --git a/demo1/test_5_0.v b/examples/demo1/test_5_0.v
similarity index 100%
rename from demo1/test_5_0.v
rename to examples/demo1/test_5_0.v
diff --git a/demo1/test_5_3.v b/examples/demo1/test_5_3.v
similarity index 100%
rename from demo1/test_5_3.v
rename to examples/demo1/test_5_3.v
diff --git a/demo1/user_0.v b/examples/demo1/user_0.v
similarity index 100%
rename from demo1/user_0.v
rename to examples/demo1/user_0.v
diff --git a/demo1/user_3.v b/examples/demo1/user_3.v
similarity index 100%
rename from demo1/user_3.v
rename to examples/demo1/user_3.v
diff --git a/demo2/classical.v b/examples/demo2/classical.v
similarity index 100%
rename from demo2/classical.v
rename to examples/demo2/classical.v
diff --git a/demo2/stage10.v b/examples/demo2/stage10.v
similarity index 98%
rename from demo2/stage10.v
rename to examples/demo2/stage10.v
index 95932c8f0..07532f604 100644
--- a/demo2/stage10.v
+++ b/examples/demo2/stage10.v
@@ -1,6 +1,6 @@
 From Coq Require Import ssreflect ssrfun ssrbool ZArith QArith.
 From HB Require Import structures.
-From HB.demo2 Require Import classical.
+From HB Require Import demo2.classical.
 
 Declare Scope hb_scope.
 Delimit Scope hb_scope with G.
@@ -10,8 +10,6 @@ Local Open Scope hb_scope.
 
 Module Stage10.
 
-HB.structure Definition TYPE := { A of True }.
-
 HB.mixin Record AddAG_of_TYPE A := {
   zero : A;
   add : A -> A -> A;
diff --git a/demo2/stage11.v b/examples/demo2/stage11.v
similarity index 99%
rename from demo2/stage11.v
rename to examples/demo2/stage11.v
index cf244e99d..f425df6f6 100644
--- a/demo2/stage11.v
+++ b/examples/demo2/stage11.v
@@ -1,6 +1,6 @@
 From Coq Require Import ssreflect ssrfun ssrbool ZArith QArith.
 From HB Require Import structures.
-From HB.demo2 Require Import classical.
+From HB Require Import demo2.classical.
 
 Declare Scope hb_scope.
 Delimit Scope hb_scope with G.
@@ -10,8 +10,6 @@ Local Open Scope hb_scope.
 
 Module Stage11.
 
-HB.structure Definition TYPE := { A of True }.
-
 HB.mixin Record AddAG_of_TYPE A := {
   zero : A;
   add : A -> A -> A;
diff --git a/demo3/hierarchy_0.v b/examples/demo3/hierarchy_0.v
similarity index 100%
rename from demo3/hierarchy_0.v
rename to examples/demo3/hierarchy_0.v
diff --git a/demo3/hierarchy_1.v b/examples/demo3/hierarchy_1.v
similarity index 100%
rename from demo3/hierarchy_1.v
rename to examples/demo3/hierarchy_1.v
diff --git a/demo3/hierarchy_2.v b/examples/demo3/hierarchy_2.v
similarity index 100%
rename from demo3/hierarchy_2.v
rename to examples/demo3/hierarchy_2.v
diff --git a/demo3/test_0_0.v b/examples/demo3/test_0_0.v
similarity index 100%
rename from demo3/test_0_0.v
rename to examples/demo3/test_0_0.v
diff --git a/demo3/test_1_0.v b/examples/demo3/test_1_0.v
similarity index 100%
rename from demo3/test_1_0.v
rename to examples/demo3/test_1_0.v
diff --git a/demo3/test_2_0.v b/examples/demo3/test_2_0.v
similarity index 100%
rename from demo3/test_2_0.v
rename to examples/demo3/test_2_0.v
diff --git a/demo3/user_0.v b/examples/demo3/user_0.v
similarity index 100%
rename from demo3/user_0.v
rename to examples/demo3/user_0.v
diff --git a/demo4/hierarchy_0.v b/examples/demo4/hierarchy_0.v
similarity index 100%
rename from demo4/hierarchy_0.v
rename to examples/demo4/hierarchy_0.v
diff --git a/demo5/hierarchy_0.v b/examples/demo5/hierarchy_0.v
similarity index 98%
rename from demo5/hierarchy_0.v
rename to examples/demo5/hierarchy_0.v
index 8bd66c73a..65f54c00e 100644
--- a/demo5/hierarchy_0.v
+++ b/examples/demo5/hierarchy_0.v
@@ -1,8 +1,6 @@
 From Coq Require Import ssreflect ssrfun.
 From HB Require Import structures.
 
-HB.structure Definition TYPE := { A of True }.
-
 HB.mixin Record AddComoid_of_TYPE A := {
   zero : A;
   add : A -> A -> A;
diff --git a/readme.v b/examples/readme.v
similarity index 100%
rename from readme.v
rename to examples/readme.v
diff --git a/hb.elpi b/hb.elpi
index 48cc381c6..c3ed077b3 100644
--- a/hb.elpi
+++ b/hb.elpi
@@ -395,7 +395,13 @@ distribute-w-params (w-params.nil N T F) L :-
 pred w-params_1 i:one-w-params A, o:A.
 w-params_1 X Y :- w-params.then X ignore ignore (p\ t\ triple_1) Y.
 
-% no implicit arguments
+
+pred hb-set-implicit i:gref, i:list implicit_kind.
+hb-set-implicit GR I :-  std.do! [
+  coq.arguments.set-implicit GR [I],
+].
+
+
 pred hb-add-const i:id, i:term, i:term, i:opaque?, o:constant.
 hb-add-const Name Bo Ty Opaque C :- std.do! [
   % TODO: refine when we switch to add-section-variable/add-const
@@ -403,7 +409,16 @@ hb-add-const Name Bo Ty Opaque C :- std.do! [
     (coq.error "HB: cannot infer some information in" Name ":" {coq.term->string Ty} ":=" {coq.term->string Bo})
     true,
   coq.env.add-const Name Bo Ty Opaque C,
-  coq.arguments.set-implicit (const C) [[]]
+  if (var Ty) (Ty? = none) (Ty? = some Ty),
+  hb-set-implicit (const C) [],
+].
+
+pred hb-add-variable i:id, i:term, o:constant.
+hb-add-variable Name Ty C :- std.do! [
+  if (Name = "_") (ID is "fresh_name_" ^ {std.any->string {new_int}}) (ID = Name),
+  % coq.env.add-section-variable ID Ty C, coq-elpi >= 1.9.x
+  @local! => coq.env.add-const ID _ Ty @opaque! C,
+  hb-set-implicit (const C) [],
 ].
 
 pred hb-add-indt i:indt-decl, o:inductive.
@@ -414,11 +429,54 @@ hb-add-indt Decl I :- std.do! [
   coq.env.add-indt Decl I,
 ].
 
+pred hb-begin-module i:id.
+hb-begin-module Name :- std.do! [
+  coq.env.begin-module Name none,
+].
+
+pred hb-end-module i:id, o:modpath.
+hb-end-module _ M :- std.do! [
+  coq.env.end-module M,
+].
+
+pred hb-begin-section i:id.
+hb-begin-section Name :- std.do! [
+  coq.env.begin-section Name,
+].
+
+pred hb-end-section i:id.
+hb-end-section _ :- std.do! [
+  coq.env.end-section,
+].
+
+pred hb-declare-instance i:gref.
+hb-declare-instance GR  :- std.do! [
+  coq.CS.declare-instance GR,
+].
+
+pred hb-add-abbreviation i:id, i:int, i:term, i:bool, o:abbreviation.
+hb-add-abbreviation Name NArgs Body OnlyParsing O :- std.do! [
+  coq.notation.add-abbreviation Name NArgs Body OnlyParsing O,
+].
+
+
+pred hb-export-module i:modpath.
+hb-export-module M :- std.do! [
+  coq.env.export-module M,
+].
+
+pred hb-coercion-declare i:coercion.
+hb-coercion-declare C :- std.do! [
+  coq.coercion.declare C,
+].
+
 %%%%%%%%% HB database %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 %Specialize coq.elpi.accumulate to "hiearchy.db"
-pred acc i:scope, i:clause.
-acc S CL :- coq.elpi.accumulate S "hb.db" CL.
+pred hb-accumulate i:scope, i:clause.
+hb-accumulate S CL :- std.do! [
+  coq.elpi.accumulate S "hb.db" CL,
+].
 
 pred from_mixin i:prop, o:mixinname.
 from_mixin (from _ X _) X.
@@ -936,7 +994,7 @@ mk-phant-abbrev N (phant-term AL T1) C Abbrev :- std.do! [
   std.assert-ok! (coq.elaborate-skeleton T1 TTy T) "mk-phant-abbrev: T illtyped",
   hb-add-const NC T TTy @transparent! C,
   mk-phant-abbrev.term 0 (global (const C)) AL NParams AbbrevT,
-  @global! => coq.notation.add-abbreviation N NParams AbbrevT tt Abbrev,
+  @global! => hb-add-abbreviation N NParams AbbrevT tt Abbrev,
 ].
 
 % [acc-phant-abbrev Str GR PhGR Abbrev] makes a phantom abbreviation for F
@@ -1139,7 +1197,7 @@ declare-instances T [class Class Struct MLwP|Rest] [CS|L] :-
   std.assert-ok! (coq.typecheck S STy) "declare-instances: S illtyped",
 
   hb-add-const Name S STy @transparent! CS, % Bug coq/coq#11155, could be a Let
-  coq.CS.declare-instance (const CS), % Bug coq/coq#11155, should be local
+  hb-declare-instance (const CS), % Bug coq/coq#11155, should be local
   declare-instances T Rest L.
 declare-instances T [_|Rest] L :- declare-instances T Rest L.
 declare-instances _ [] [].
@@ -1151,10 +1209,10 @@ type factory-by-phantabbrev abbreviation -> factory-abbrev.
 pred declare-factory-abbrev i:id, i:factory-abbrev.
 declare-factory-abbrev Name (factory-by-classname GR) :-
   % looks fishy (the parameters are not taken into account)
-  @global! => coq.notation.add-abbreviation Name 1 (fun _ _ t\ app[global GR,t]) tt _.
+  @global! => hb-add-abbreviation Name 1 (fun _ _ t\ app[global GR,t]) tt _.
 declare-factory-abbrev Name (factory-by-phantabbrev Abbr) :- std.do! [
   coq.notation.abbreviation-body Abbr Nargs AbbrTrm,
-  @global! => coq.notation.add-abbreviation Name Nargs AbbrTrm tt _,
+  @global! => hb-add-abbreviation Name Nargs AbbrTrm tt _,
 ].
 
 % [mk-factory-abbrev Str GR CL FactAbbrev]
@@ -1192,7 +1250,7 @@ postulate-arity (parameter ID _ S A) Acc T T1 Ty :-
   std.assert-ok! (coq.typecheck-ty S _) "arity parameter illtyped",
   if-verbose (coq.say "HB: postulating" ID),
   if (var S) (coq.fresh-type S) true,
-  @local! => hb-add-const ID _ S @opaque! C,
+  hb-add-variable ID S C,
   Var = global (const C),
   postulate-arity (A Var) [Var|Acc] T T1 Ty.
 postulate-arity (arity Ty) ArgsRev X T Ty :-
@@ -1211,7 +1269,7 @@ postulate-mixin (triple M Ps T) MSL [mixin-src T M (global (const C))|MSL] :- MS
 
   mgref->term Ps T M Ty,
   std.assert-ok! (coq.typecheck Ty _) "postulate-mixin: Ty illtyped",
-  @local! => hb-add-const Name _ Ty @opaque! C % no body, local -> a variable
+  hb-add-variable Name Ty C
 ].
 
 % [main-declare-context TheType Parameters Factories Clauses] postulates a
@@ -1224,7 +1282,7 @@ main-declare-context TheType TheParams GRFSwP MSL CL :-  std.do! [
   apply-w-params MLwP TheParams TheType MLwAllArgs,
   std.fold MLwAllArgs [] postulate-mixin MSL,
   MSL => declare-instances TheType {findall-classes} CL,
-  std.forall MSL (ms\ acc current (clause _ _ ms)),
+  std.forall MSL (ms\ hb-accumulate current (clause _ _ ms)),
 ].
 
 % [main-declare-builder (builder _ F M B) From MoreFrom] Given B of type FB, it
@@ -1249,8 +1307,8 @@ main-declare-builder (builder _ SrcFactory TgtMixin B) FromClauses MoreFromClaus
 pred to-export o:modpath.
 pred export i:modpath.
 export Module :- !,
-  coq.env.export-module Module,
-  acc current (clause _ _ (to-export Module)).
+  hb-export-module Module,
+  hb-accumulate current (clause _ _ (to-export Module)).
 
 pred main-reexport.
 main-reexport :- !,
@@ -1315,7 +1373,7 @@ export-1-operation M Struct Psort Pclass MwP (some Poperation) EXI EXO :- !, std
   w-params.nparams MwP NP,
   NImplicits is NP + 1,
   std.map {std.iota NImplicits} (_\r\ r = maximal) Implicits,
-  @global! => coq.arguments.set-implicit (const C) [Implicits],
+  @global! => hb-set-implicit (const C) Implicits,
 
   EXO = [exported-op M Poperation C|EXI]
 ].
@@ -1396,7 +1454,7 @@ pred declare-coercion i:term, i:term, i:class, i:class.
 declare-coercion SortProjection ClassProjection
     (class FC StructureF FMLwP) (class TC StructureT TMLwP) :- std.do! [
 
-  acc current (clause _ _ (sub-class FC TC)),
+  hb-accumulate current (clause _ _ (sub-class FC TC)),
 
   gref->modname StructureF ModNameF,
   gref->modname StructureT ModNameT,
@@ -1413,7 +1471,7 @@ declare-coercion SortProjection ClassProjection
   if-verbose (coq.say "HB: declare coercion hint" CName),
 
   hb-add-const CName CoeBody Ty @transparent! C,
-  @global! => coq.coercion.declare (coercion (const C) 1 FC (grefclass TC)),
+  @global! => hb-coercion-declare (coercion (const C) 1 FC (grefclass TC)),
 
   Coercion = global (const C),
   w-params.then FMLwP mk-fun ignore
@@ -1425,8 +1483,8 @@ declare-coercion SortProjection ClassProjection
   if-verbose (coq.say "HB: declare unification hint" SName),
 
   hb-add-const SName SCoeBody STy @transparent! SC,
-  @global! => coq.coercion.declare (coercion (const SC) 0 StructureF (grefclass StructureT)),
-  coq.CS.declare-instance (const SC), % TODO: API in Elpi, take a @constant instead of gref
+  @global! => hb-coercion-declare (coercion (const SC) 0 StructureF (grefclass StructureT)),
+  hb-declare-instance (const SC), % TODO: API in Elpi, take a @constant instead of gref
 ].
 
 pred join-body i:int, i:int, i:structure, i:term, i:term, i:term, i:term, i:term,
@@ -1464,7 +1522,7 @@ declare-join (class C3 S3 MLwP3) (pr (class C1 S1 _) (class C2 S2 _)) (join C1 C
     (global S2_Pack) S1_sort S3_to_S1 S2_class S3_to_S2) JoinBody,
   std.assert-ok! (coq.typecheck JoinBody Ty) "declare-join: JoinBody illtyped",
   hb-add-const Name JoinBody Ty @transparent! J,
-  coq.CS.declare-instance (const J).
+  hb-declare-instance (const J).
 
 % TODO: this works under the invariant: we never have two classes that
 % contain exactly the same mixins. hb.structure should enforce this
@@ -1546,7 +1604,7 @@ declare-sort-coercion StructureName (global Proj) :-
 
   if-verbose (coq.say "HB: declare sort coercion"),
 
-  @global! => coq.coercion.declare (coercion Proj 0 StructureName sortclass).
+  @global! => hb-coercion-declare (coercion Proj 0 StructureName sortclass).
 
 pred if-class-already-exists-error i:id, i:list class, i:list mixinname.
 if-class-already-exists-error _ [] _.
@@ -1563,27 +1621,27 @@ export-mixin-coercion ClassName (some C) :-
   head-gref-under-prods CTy MixinGR,
   if-verbose (coq.say "HB: export class to mixin coercion for mixin" {nice-gref->string MixinGR}),
   @global! =>
-    coq.coercion.declare (coercion (const C) _ ClassName (grefclass MixinGR)).
+    hb-coercion-declare (coercion (const C) _ ClassName (grefclass MixinGR)).
 
 pred mc-compat-structure i:string, i:modpath, i:list mixinname, i:int, i:classname, i:term, i:option gref.
 mc-compat-structure ModuleName _Module NewMixins CNParams ClassName ClassProjection Axioms :- std.do! [
   CompatModuleName is "MathCompCompat" ^ ModuleName,
-  coq.env.begin-module CompatModuleName none, % to avoid collisions
-  coq.env.begin-module ModuleName none,
+  hb-begin-module CompatModuleName, % to avoid collisions
+  hb-begin-module ModuleName,
 
   if (Axioms = some GR)
-    (@global! => coq.notation.add-abbreviation "axiom" 0 (global GR) ff _)
+    (@global! => hb-add-abbreviation "axiom" 0 (global GR) ff _)
     true,
 
   if (NewMixins = [NewMixin]) (std.do! [
     if-verbose (coq.say "mc-compat-structure: declaring notations 'axioms', 'mixin_of' and 'Mixin'"),
     MArgs is {factory-nparams NewMixin} + 1,
     mk-eta MArgs {coq.env.typeof NewMixin} (global NewMixin) EtaNewMixin,
-    @global! => coq.notation.add-abbreviation "axioms" MArgs EtaNewMixin ff _,
-    @global! => coq.notation.add-abbreviation "mixin_of" MArgs EtaNewMixin ff _,
+    @global! => hb-add-abbreviation "axioms" MArgs EtaNewMixin ff _,
+    @global! => hb-add-abbreviation "mixin_of" MArgs EtaNewMixin ff _,
     std.assert! (factory-constructor NewMixin FK) "BUG: Factory constructor missing",
     std.assert! (phant-abbrev FK _ PhAbb) "BUG: missing phant-abbrev",
-    @global! => coq.notation.add-abbreviation "Mixin" 0
+    @global! => hb-add-abbreviation "Mixin" 0
       {coq.notation.abbreviation PhAbb {coq.mk-n-holes MArgs}} ff _,
     if-verbose (coq.say "mc-compat-structure: declaring pack abbreviation"),
     class-def (class ClassName _ ClassMixins),
@@ -1597,11 +1655,11 @@ mc-compat-structure ModuleName _Module NewMixins CNParams ClassName ClassProject
   std.assert-ok! (coq.typecheck ClassProjection ClassProjectionTy) "wtf",
   CArgs is CNParams + 1,
   mk-eta CArgs ClassProjectionTy ClassProjection EtaClassProjection,
-  @global! => coq.notation.add-abbreviation "class_of" CArgs EtaClassProjection ff _,
+  @global! => hb-add-abbreviation "class_of" CArgs EtaClassProjection ff _,
 
-  coq.env.end-module _,
-  coq.env.end-module MCCompat,
-  coq.env.export-module MCCompat,
+  hb-end-module ModuleName _,
+  hb-end-module CompatModuleName MCCompat,
+  hb-export-module MCCompat,
   %coq.env.import-module Module,
 ].
 
@@ -1681,7 +1739,7 @@ main-declare-structure Module GRFSwP ClosureCheck :- std.do! [
 
   if-verbose (coq.say "HB: start module" Module),
 
-  coq.env.begin-module Module none,
+  hb-begin-module Module,
 
   declare-class+structure MLwP
     ClassName Structure SortProjection ClassProjection Factories,
@@ -1703,7 +1761,7 @@ main-declare-structure Module GRFSwP ClosureCheck :- std.do! [
 
   if-verbose (coq.say "HB: start module Exports"),
 
-  coq.env.begin-module "Exports" none,
+  hb-begin-module "Exports",
   declare-sort-coercion Structure SortProjection,
 
   if-verbose (coq.say "HB: exporting unification hints"),
@@ -1725,12 +1783,12 @@ main-declare-structure Module GRFSwP ClosureCheck :- std.do! [
       NewJoins, [class-def CurrentClass], GRDepsClauses
     ]
     NewClauses,
-  std.forall NewClauses (c\ acc current (clause _ _ c)),
+  std.forall NewClauses (c\ hb-accumulate current (clause _ _ c)),
 
   if-verbose (coq.say "HB: stop module Exports"),
-  coq.env.end-module Exports,
+  hb-end-module "Exports" Exports,
 
-  coq.env.end-module ModulePath,
+  hb-end-module Module ModulePath,
 
   if-verbose (coq.say "HB: end modules; export" Exports),
 
@@ -1745,10 +1803,10 @@ main-declare-structure Module GRFSwP ClosureCheck :- std.do! [
   if-verbose (coq.say "HB: operations meta-data module: ElpiOperations"),
 
   ElpiOperationModName is "ElpiOperations" ^ {std.any->string {new_int}},
-  coq.env.begin-module ElpiOperationModName none,
+  hb-begin-module ElpiOperationModName,
     std.map MLToExport (m\r\ r = mixin-first-class m ClassName) MixinFirstClass,
-    std.forall {std.append EX MixinFirstClass} (c\ acc current (clause _ _ c)),
-  coq.env.end-module ElpiOperations,
+    std.forall {std.append EX MixinFirstClass} (c\ hb-accumulate current (clause _ _ c)),
+  hb-end-module ElpiOperationModName ElpiOperations,
   export ElpiOperations,
 
   if-verbose (coq.say "HB: abbreviation factory-by-classname"),
@@ -1765,23 +1823,23 @@ main-begin-declare Module TName GRFS Decl :- std.do! [
 
   if-verbose (coq.say "HB: start module and section" Module),
 
-  coq.env.begin-module Module none,
-  coq.env.begin-section Module,
+  hb-begin-module Module none,
+  hb-begin-section Module,
 
   if-verbose (coq.say "HB: postulate type" TName),
 
   coq.fresh-type Ty,
   @local! => hb-add-const TName _ Ty @opaque! T, % no body, local -> a variable
   main-declare-context (global (const T)) [] GRFS _, % TODO params
-  acc current (clause _ _ (current-mode Decl))
+  hb-accumulate current (clause _ _ (current-mode Decl))
 ].
 */
 
 pred main-end-declare-builders.
 main-end-declare-builders :- std.do! [
-  current-mode (builder-from _ GR),
+  current-mode (builder-from _ GR ModName),
 
-  coq.env.end-section,
+  hb-end-section ModName,
 
   findall-builders LFIL,
 
@@ -1794,11 +1852,11 @@ main-end-declare-builders :- std.do! [
   % TODO: Do we need this module?
   gref->modname GR M,
   Name is M ^ "_Exports",
-  coq.env.begin-module Name none,
-  (std.forall Clauses c\ acc current (clause _ _ c)),
+  hb-begin-module Name,
+  (std.forall Clauses c\ hb-accumulate current (clause _ _ c)),
 
-  coq.env.end-module Exports,
-  coq.env.end-module _,
+  hb-end-module Name Exports,
+  hb-end-module ModName _,
   export Exports,
 ].
 
@@ -1822,7 +1880,7 @@ add-mixin T FGR MakeCanon MissinMixin Bo [MixinSrcCl, BuiderDeclCl] :-
      hb-add-const Name Bo Ty @transparent! C),
   if (MakeCanon = tt, whd (global (const C)) [] (global (indc _)) _)
      (if-verbose (coq.say "HB: declare canonical mixin instance" C),
-      coq.CS.declare-instance (const C))
+      hb-declare-instance (const C))
      true.
 
 pred mixin-for_mixin-builder i:prop, o:term.
@@ -1872,19 +1930,19 @@ declare-canonical-instances-from-factory T F :-
 
 % entry point for HB.instance
 pred main-declare-instance i:term, i:term, o:list prop.
-main-declare-instance T F Clauses :- current-mode (builder-from TheFactory FGR), !,
+main-declare-instance T F Clauses :- current-mode (builder-from TheFactory FGR _), !,
   declare-canonical-instances-from-factory-and-local-builders T F TheFactory FGR Clauses.
 main-declare-instance T F [] :-
   declare-canonical-instances-from-factory T F.
 
 pred declare-old-located i:string, i:located.
 declare-old-located Id (loc-gref GR) :-
-  @global! => coq.notation.add-abbreviation Id 0 (global GR) ff _.
+  @global! => hb-add-abbreviation Id 0 (global GR) ff _.
 declare-old-located Id (loc-abbreviation Abbrev) :-
   coq.notation.abbreviation Abbrev [] T,
   % FIXME: this assumes the abbreviation has no arg
   % we should fix it.
-  @global! => coq.notation.add-abbreviation Id 0 T ff _.
+  @global! => hb-add-abbreviation Id 0 T ff _.
 
 pred declare-old-constant i:option constant.
 declare-old-constant none.
@@ -1920,17 +1978,17 @@ main-begin-declare-builders CtxSkel :- std.do! [
   Name is "Builders_" ^ {term_to_string {new_int}}, % TODO?
   std.assert-ok! (elaborate-context-skel->factory CtxSkel Ctx GRF) "Context illtyped",
   if-verbose (coq.say "HB: context to factory"),
-  coq.env.begin-module Name none,
+  hb-begin-module Name,
   if-verbose (coq.say "HB: begin module for builders"),
   if (GRF = indt FRecord) (std.do! [
     if-verbose (coq.say "HB: begin module Super"),
-    coq.env.begin-module "Super" none,
+    hb-begin-module "Super",
     std.forall {coq.CS.canonical-projections FRecord} declare-old-constant,
-    coq.env.end-module _,
+    hb-end-module "Super" _,
     if-verbose (coq.say "HB: ended module Super")]) (true),
-  coq.env.begin-section Name,
+  hb-begin-section Name,
   if-verbose (coq.say "HB: postulating factories"),
-  builders-postulate-factories Ctx,
+  builders-postulate-factories Name Ctx,
 ].
 
 pred postulate-factory-abbrev i:term, i:list term, i:id, i:factoryname, o:term.
@@ -1940,7 +1998,7 @@ postulate-factory-abbrev TheType Params Name Falias TheFactory :- std.do! [
   coq.notation.abbreviation Fabv {std.append Params [TheType]} Package,
   Msg is "Unable to declare factory " ^ Name,
   std.assert-ok! (coq.typecheck-ty Package _) Msg,
-  @local! => hb-add-const Name _ Package @opaque! C,
+  hb-add-variable Name Package C,
   TheFactory = global (const C),
 ].
 
@@ -1962,21 +2020,21 @@ define-factory-operation TheType Params TheFactory NHoles (some P) :-
   T = app[global (const P)|Args],
   std.assert-ok! (coq.typecheck T _) "Illtyped applied factory operation",
   coq.gref->id (const P) Name,
-  @local! => coq.notation.add-abbreviation Name 0 T ff _.
+  @local! => hb-add-abbreviation Name 0 T ff _.
 
 pred fresh-type o:term.
 fresh-type Ty :-
   Ty = {{Type}},
   std.assert-ok! (coq.typecheck-ty Ty _) "impossible".
 
-pred builders-postulate-factories i:context-decl.
-builders-postulate-factories (context-item IDT _ TySkel none t\ context-item IDF _ (TF t) none _\ context-end) :- !, std.do! [
+pred builders-postulate-factories i:id, i:context-decl.
+builders-postulate-factories ModName (context-item IDT _ TySkel none t\ context-item IDF _ (TF t) none _\ context-end) :- !, std.do! [
   % TODO we should allow T to be anything.
   std.assert-ok! (coq.elaborate-ty-skeleton TySkel _ Ty) "builders-postulate-factory: illtyped context",
   if (var Ty) (fresh-type Ty)
      (std.assert-ok! (coq.unify-eq Ty {{Type}}) "The last context item before the factory must be a type variable"),
   if-verbose (coq.say "HB: postulating type" IDT),
-  @local! => hb-add-const IDT _ Ty @opaque! C, % no body, local -> a variable
+  hb-add-variable IDT Ty C,
   TheType = global (const C),
 
   std.assert! (factory? (TF TheType) (triple GRF Params TheType))
@@ -1985,19 +2043,19 @@ builders-postulate-factories (context-item IDT _ TySkel none t\ context-item IDF
   main-declare-context TheType Params GRFMLwP _ _,
   postulate-factory-abbrev TheType Params IDF GRF TheFactory,
   define-factory-operations TheType Params TheFactory GRF,
-  acc current (clause _ _ (current-mode (builder-from TheFactory GRF))),
+  hb-accumulate current (clause _ _ (current-mode (builder-from TheFactory GRF ModName))),
 ].
 
-builders-postulate-factories (context-item ID _ TSkel none Factories) :- std.do! [
+builders-postulate-factories ModName (context-item ID _ TSkel none Factories) :- std.do! [
   if-verbose (coq.say "HB: postulating" ID),
   std.assert-ok! (coq.elaborate-ty-skeleton TSkel _ T) "builders-postulate-factories: illtyped context",
   if (var T) (coq.fresh-type T) true,
-  @local! => hb-add-const ID _ T @opaque! P, % no body, local -> a variable
+  hb-add-variable ID T P,
   TheParam = global (const P),
-  builders-postulate-factories (Factories TheParam),
+  builders-postulate-factories ModName (Factories TheParam),
 ].
 
-builders-postulate-factories (context-item ID _ _ (some _) _) :-
+builders-postulate-factories _ (context-item ID _ _ (some _) _) :-
   coq.error "context item cannot be given a body:" ID.
 
 % In an asset like HB.mixing Recoord P1 .. PN A of F1 .. & FK ..
@@ -2016,8 +2074,8 @@ main-declare-asset Asset AssetKind :- std.do! [
 
   if-verbose (coq.say "HB: start module and section" Module),
 
-  coq.env.begin-module Module none,
-  coq.env.begin-section Module,
+  hb-begin-module Module,
+  hb-begin-section Module,
 
   % We start by postulating the parameters
   process-asset-named-parameters Asset AssetKind Module [],
@@ -2029,7 +2087,7 @@ process-asset-named-parameters (asset-parameter Name T Rest as R) D Module Param
 
   if-verbose (coq.say "HB: postulate type" Name),
   if (var T) (fresh-type Ty) (Ty = T),
-  @local! => hb-add-const Name _ Ty @opaque! C, % no body, local -> a variable
+  hb-add-variable Name Ty C,
 
   TheType = global (const C),
   % We postulate the dependencies
@@ -2040,7 +2098,7 @@ process-asset-named-parameters (asset-parameter Name T Rest) D Module Params :-
   std.assert-ok! (coq.typecheck-ty T _) "Illtyped parameter",
   if-verbose (coq.say "HB: postulate " Name),
   if (var T) (coq.fresh-type T) true,
-  @local! => hb-add-const Name _ T @opaque! C, % no body, local -> a variable
+  hb-add-variable Name T C,
   TheParam = global (const C),
   process-asset-named-parameters (Rest TheParam) D Module [triple Name TheParam T|Params],
 ].
@@ -2085,7 +2143,7 @@ declare-factory-alias Ty1Skel GRFSwP Module TheType TheParams :- std.do! [
   hb-add-const "Axioms_" MFK MFKTyC @transparent! CK,
   GRK = const CK,
 
-  coq.env.end-section,
+  hb-end-section Module,
 
   @global! => coq.arguments.set-implicit GRK [[]],
 
@@ -2101,17 +2159,17 @@ declare-factory-alias Ty1Skel GRFSwP Module TheType TheParams :- std.do! [
 
   if-verbose (coq.say "HB: start module Exports"),
 
-  coq.env.begin-module "Exports" none,
-  std.forall Clauses (c\ acc current (clause _ _ c)),
-  std.forall GRDepsClauses (c\ acc current (clause _ _ c)),
+  hb-begin-module "Exports",
+  std.forall Clauses (c\ hb-accumulate current (clause _ _ c)),
+  std.forall GRDepsClauses (c\ hb-accumulate current (clause _ _ c)),
   % std.map {gr-deps GRK} (_\ r\ r = maximal) Implicits,
-  % coq.arguments.set-implicit GRK [[maximal|Implicits]] tt,
+  % hb-set-implicit GRK [maximal|Implicits],
   w-params.nparams MLwP NParams,
-  acc current (clause _ _ (factory-nparams (const C) NParams)),
-  acc current (clause _ _ (factory-constructor (const C) GRK)),
-  acc current (clause _ _ (factory-builder-nparams BuildConst NParams)),
-  coq.env.end-module Exports,
-  coq.env.end-module _Module,
+  hb-accumulate current (clause _ _ (factory-nparams (const C) NParams)),
+  hb-accumulate current (clause _ _ (factory-constructor (const C) GRK)),
+  hb-accumulate current (clause _ _ (factory-builder-nparams BuildConst NParams)),
+  hb-end-module "Exports" Exports,
+  hb-end-module Module _,
 
   if-verbose (coq.say "HB: end modules and sections; export" Exports),
 
@@ -2212,14 +2270,14 @@ declare-mixin-or-factory Sort1 Fields GRFSwP Module TheType D TheParams :- std.d
   copy-clauses-for-unfold SectionCanonicalInstance CopyUnfold,
   CopyUnfold => abstract-indt-decl Section RDecl RDeclClosed,
   hb-add-indt RDeclClosed R,
-  coq.env.end-section, % We need to anyway declare the record inside the section
+  hb-end-section Module, % We need to anyway declare the record inside the section
     % since closing the section purges the unused universe level we may have
     % allocated by typechecking the skeleton just above
 
   coq.env.indt R tt _ _ _ [K] _,
   GRK = indc K,
-  @global! => coq.arguments.set-implicit (indt R) [[]],
-  @global! => coq.arguments.set-implicit GRK [[]],
+  @global! => hb-set-implicit (indt R) [],
+  @global! => hb-set-implicit GRK [],
 
   factories-provide GRFSwP MLwP,
   w-params.nparams MLwP NParams,
@@ -2243,17 +2301,17 @@ declare-mixin-or-factory Sort1 Fields GRFSwP Module TheType D TheParams :- std.d
 
   if-verbose (coq.say "HB: start module Exports"),
 
-  coq.env.begin-module "Exports" none,
-  std.forall Clauses (c\ acc current (clause _ _ c)),
-  std.forall GRDepsClauses (c\ acc current (clause _ _ c)),
-  acc current (clause _ _ (factory-nparams (indt R) NParams)),
+  hb-begin-module "Exports",
+  std.forall Clauses (c\ hb-accumulate current (clause _ _ c)),
+  std.forall GRDepsClauses (c\ hb-accumulate current (clause _ _ c)),
+  hb-accumulate current (clause _ _ (factory-nparams (indt R) NParams)),
   std.map {list-w-params_list MLwP} (_\ r\ r = maximal) Implicits,
-  @global! => coq.arguments.set-implicit GRK [[maximal|Implicits]],
-  acc current (clause _ _ (factory-constructor (indt R) GRK)),
-  acc current (clause _ _ (factory-builder-nparams BuildConst NParams)),
-  acc current (clause _ _ (phant-abbrev GRK (const BuildConst) BuildAbbrev)),
-  coq.env.end-module Exports,
-  coq.env.end-module _Module,
+  @global! => hb-set-implicit GRK [maximal|Implicits],
+  hb-accumulate current (clause _ _ (factory-constructor (indt R) GRK)),
+  hb-accumulate current (clause _ _ (factory-builder-nparams BuildConst NParams)),
+  hb-accumulate current (clause _ _ (phant-abbrev GRK (const BuildConst) BuildAbbrev)),
+  hb-end-module "Exports" Exports,
+  hb-end-module Module _,
 
   if-verbose (coq.say "HB: end modules and sections; export" Exports),
 
@@ -2261,3 +2319,56 @@ declare-mixin-or-factory Sort1 Fields GRFSwP Module TheType D TheParams :- std.d
 
   GRDepsClauses => declare-factory-abbrev Module FactAbbrev,
 ].
+
+
+% If you don't mention the factory in a builder, then Coq won't make
+% a lambda for it at section closing time.
+pred hack-section-discharging i:term, o:term.
+hack-section-discharging B B1 :- current-mode (builder-from TheFactory _ _), !,
+  std.assert-ok! (coq.typecheck TheFactory TheFactoryTy) "TheFactory is illtyped (BUG)",
+  B1 = {{ let _ : lp:TheFactoryTy := lp:TheFactory in lp:B }}.
+hack-section-discharging B B.
+
+pred optimize-body i:term, o:term.
+optimize-body (app[global (const C)| Args]) Red :- phant-abbrev _ (const C) _, !,
+  coq.env.const C (some B) _,
+  hd-beta B Args HD Stack,
+  unwind HD Stack Red.
+optimize-body X X.
+
+pred main-declare-const-instance i:id, i:term, i:arity.
+main-declare-const-instance Name BodySkel TyWPSkel :- std.do! [
+  std.assert-ok! (coq.elaborate-arity-skeleton TyWPSkel _ TyWP) "Definition type illtyped",
+  coq.arity->term TyWP Ty,
+  std.assert-ok! (coq.elaborate-skeleton BodySkel Ty Body) "Definition illtyped",
+  if (TyWP = arity SectionTy) (
+     % Do not open a section when it is not necessary (no parameters)
+     % A side effect of opening a section is loosing meta data associated
+     % with instances, in particular builder tags are lost
+     if-verbose (coq.say  "HB: skipping section opening"),
+     SectionBody = Body
+   ) (
+    SectionName is "hb_instance_" ^ {term_to_string {new_int} },
+    hb-begin-section SectionName,
+    postulate-arity TyWP [] Body SectionBody SectionTy
+  ),
+
+  std.assert! (coq.safe-dest-app SectionTy (global FactoryAlias) Args) "The type of the instance is not a factory",
+  factory-alias->gref FactoryAlias Factory,
+  std.assert! (factory-nparams Factory NParams) "Not a factory synthesized by HB",
+  hack-section-discharging SectionBody SectionBodyHack,
+  optimize-body SectionBodyHack OptimizedBody,
+  if (Name = "_") (RealName is "HB_unnamed_factory_" ^ {std.any->string {new_int} }) (RealName = Name),
+  hb-add-const RealName OptimizedBody _ @transparent! C,
+  TheFactory = (global (const C)),
+  std.appendR {coq.mk-n-holes NParams} [TheType|_] Args,
+  main-declare-instance TheType TheFactory Clauses,
+
+  if (TyWP = arity _) true (
+    if-verbose (coq.say "HB: closing instance section"),
+    hb-end-section SectionName
+  ),
+
+  % we accumulate clauses here since the section ends
+  std.forall Clauses (x\hb-accumulate current (clause _ _ x)),
+].
diff --git a/structures.v b/structures.v
index 30e3c72e4..e1944da40 100644
--- a/structures.v
+++ b/structures.v
@@ -129,7 +129,8 @@ pred mixin-first-class o:mixinname, o:classname.
 
 % To tell HB.end what we are doing
 kind declaration type.
-type builder-from term -> factoryname -> declaration. % TheFactory and it's name
+% TheFactory and it's name and the name of the module encloding all that
+type builder-from term -> factoryname -> id -> declaration.
 pred current-mode o:declaration.
 
 pred exported-op o:mixinname, o:constant, o:constant. % memory of exported operations
@@ -327,61 +328,19 @@ Elpi Accumulate File "hb.elpi".
 Elpi Accumulate Db hb.db.
 Elpi Accumulate lp:{{
 
-% If you don't mention the factory in a builder, then Coq won't make
-% a lambda for it at section closing time.
-pred hack-section-discharging i:term, o:term.
-hack-section-discharging B B1 :- current-mode (builder-from TheFactory _), !,
-  std.assert-ok! (coq.typecheck TheFactory TheFactoryTy) "TheFactory is illtyped (BUG)",
-  B1 = {{ let _ : lp:TheFactoryTy := lp:TheFactory in lp:B }}.
-hack-section-discharging B B.
-
-pred optimize-body i:term, o:term.
-optimize-body (app[global (const C)| Args]) Red :- phant-abbrev _ (const C) _, !,
-  coq.env.const C (some B) _,
-  hd-beta B Args HD Stack,
-  unwind HD Stack Red.
-optimize-body X X.
-
 main [const-decl Name (some BodySkel) TyWPSkel] :- !, std.do! [
-  std.assert-ok! (coq.elaborate-arity-skeleton TyWPSkel _ TyWP) "Definition type illtyped",
-  coq.arity->term TyWP Ty,
-  std.assert-ok! (coq.elaborate-skeleton BodySkel Ty Body) "Definition illtyped",
-  if (TyWP = arity SectionTy) (
-     % Do not open a section when it is not necessary (no parameters)
-     % A side effect of opening a section is loosing meta data associated
-     % with instances, in particular builder tags are lost
-     with-attributes (if-verbose (coq.say  "HB: skipping section opening")),
-     SectionBody = Body
-   ) (
-    SectionName is "hb_instance_" ^ {term_to_string {new_int} },
-    coq.env.begin-section SectionName,
-    postulate-arity TyWP [] Body SectionBody SectionTy
+  with-attributes (
+      main-declare-const-instance Name BodySkel TyWPSkel
   ),
-
-  std.assert! (coq.safe-dest-app SectionTy (global FactoryAlias) Args) "The type of the instance is not a factory",
-  factory-alias->gref FactoryAlias Factory,
-  std.assert! (factory-nparams Factory NParams) "Not a factory synthesized by HB",
-  hack-section-discharging SectionBody SectionBodyHack,
-  optimize-body SectionBodyHack OptimizedBody,
-  if (Name = "_") (RealName is "HB_unnamed_factory_" ^ {std.any->string {new_int} }) (RealName = Name),
-  hb-add-const RealName OptimizedBody _ @transparent! C,
-  TheFactory = (global (const C)),
-  std.appendR {coq.mk-n-holes NParams} [TheType|_] Args,
-  with-attributes (main-declare-instance TheType TheFactory Clauses),
-
-  if (TyWP = arity _) true (
-    if-verbose (coq.say "HB: closing instance section"),
-    coq.env.end-section
+].
+main [T0, F0] :- std.do! [
+  argument->ty T0 T, % TODO: change this when supporting morphism hierarchies
+  argument->term F0 F,
+  with-attributes (
+      main-declare-instance T F Clauses,
+      std.forall Clauses (x\hb-accumulate current (clause _ _ x))
   ),
-
-  % we accumulate clauses here since the section ends
-  std.forall Clauses (x\acc current (clause _ _ x)),
 ].
-main [T0, F0] :-
-  argument->ty T0 T, !, % TODO: change this when supporting morphism hierarchies
-  argument->term F0 F, !,
-  with-attributes (main-declare-instance T F Clauses), !,
-  std.forall Clauses (x\acc current (clause _ _ x)).
 
 main _ :- coq.error "Usage: HB.instance <CarrierType> <FactoryInstanceTerm>*\nUsage: HB.instance Definition <Name> := <Builder> T ...".