From 574dcf50855934efa8134497781e912eaeddf7ec Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 11 Mar 2020 10:49:12 +0100
Subject: [PATCH 1/5] Generate an abbreviation `F X` for `F.axioms X` (fix #61)

---
 README.md |  8 +++---
 hb.elpi   | 73 +++++++++++++++++++++++++++++++++++--------------------
 readme.v  |  6 ++---
 3 files changed, 54 insertions(+), 33 deletions(-)

diff --git a/README.md b/README.md
index 23fa614f5..535d036d0 100644
--- a/README.md
+++ b/README.md
@@ -17,7 +17,7 @@ HB.mixin Record AddComoid_of_Type A := {
   addrC : forall x y, add x y = add y x;
   add0r : forall x, add zero x = x;
 }.
-HB.structure Definition AddComoid := { A of AddComoid_of_Type.axioms A }.
+HB.structure Definition AddComoid := { A of AddComoid_of_Type A }.
 
 Notation "0" := zero.
 Infix "+" := add.
@@ -32,17 +32,17 @@ We proceed by declaring how to obtain an Abelian group out of the
 additive, commutative, monoid.
 
 ```coq
-HB.mixin Record AbelianGrp_of_AddComoid A of AddComoid.axioms A := {
+HB.mixin Record AbelianGrp_of_AddComoid A of AddComoid A := {
   opp : A -> A;
   addNr : forall x, opp x + x = 0;
 }.
-HB.structure Definition AbelianGrp := { A of AbelianGrp_of_AddComoid.axioms A & }.
+HB.structure Definition AbelianGrp := { A of AbelianGrp_of_AddComoid A & }.
 
 Notation "- x" := (opp x).
 ```
 
 Abelian groups feature the operations and properties given by the
-`AbelianGrp_of_AddComoid.axioms` and `AddComoid_of_Type.axioms` mixins.
+`AbelianGrp_of_AddComoid` and `AddComoid_of_Type` mixins.
 
 ```coq
 Lemma example (G : AbelianGrp.type) (x : G) : x + (- x) = - 0.
diff --git a/hb.elpi b/hb.elpi
index 18dda8b2c..a6173747b 100644
--- a/hb.elpi
+++ b/hb.elpi
@@ -555,10 +555,9 @@ mk-phant-abbrev N (phant-term AL T) C Abbrev :- std.do! [
   add-abbrev N NParams AbbrevT tt tt Abbrev,
 ].
 
-% [acc-phant-abbrev Str GR Acc] makes a phantom abbreviation for F
-pred acc-phant-abbrev i:string, i:gref, o:list prop.
-acc-phant-abbrev _Str GR [] :- factory-alias->gref GR _, !.
-acc-phant-abbrev Str GR [phant-abbrev GR (const PhC) Abbrev] :- !, std.do! [
+% [acc-phant-abbrev Str GR PhGR Abbrev] makes a phantom abbreviation for F
+pred acc-phant-abbrev i:string, i:gref, o:gref, o:abbreviation.
+acc-phant-abbrev Str GR (const PhC) Abbrev :- !, std.do! [
   mk-phant-mixins (global GR) PhGR,
   mk-phant-abbrev Str PhGR PhC Abbrev
 ].
@@ -673,20 +672,36 @@ declare-instances T [class Class Struct ML|Rest] :-
 declare-instances T [_|Rest] :- declare-instances T Rest.
 declare-instances _ [].
 
-% [main-factory-requires Str GR FL CL]
+kind factory-name type.
+type factory-by-classname gref -> factory-name.
+type factory-by-phantabbrev abbreviation -> factory-name.
+
+pred declare-factory-abbrev i:id, i:factory-name.
+declare-factory-abbrev Name (factory-by-classname GR) :-
+  add-abbrev Name 1 (fun _ _ t\ app[global GR,t]) tt tt _.
+declare-factory-abbrev Name (factory-by-phantabbrev Abbr) :-
+  add-abbrev Name 1 (fun _ _ t\ {coq.notation.abbreviation Abbr [t]}) tt tt _.
+
+% [main-factory-requires Str GR FL CL SN]
 % computes the list of mixins ML provided by FL,
 % creates a clause in CL stating that GR requires ML (factory-requires ..), and
 % creates an abbreviation for GR names Str and creates a phant-abbrev clause in CL.
-pred main-factory-requires i:string, i:gref, i:list factoryname, o:list prop.
-main-factory-requires Str GR GRFS [FactoryRequires|Aliases] :- !, std.do! [
+% SN is the short name for the factory (either an alias of the class record)
+pred main-factory-requires i:string, i:gref, i:list factoryname, o:list prop, o:factory-name.
+main-factory-requires Str GR GRFS [FactoryRequires|Aliases] SN :- !, std.do! [
   factories-provide GRFS ML,
   FactoryRequires = factory-requires GR ML,
-  acc-phant-abbrev Str GR Aliases
+  if (factory-alias->gref GR _)
+     (Aliases = [],
+      SN = factory-by-classname GR)
+     (acc-phant-abbrev Str GR PhGR Abbrv,
+      Aliases = [phant-abbrev GR PhGR Abbrv],
+      SN = factory-by-phantabbrev Abbrv),
 ].
 
-pred main-mixin-requires i:string, i:gref, i:list factoryname, o:list prop.
-main-mixin-requires Str GR GRFS [From|PO] :- !, std.do! [
-  main-factory-requires Str GR GRFS PO,
+pred main-mixin-requires i:string, i:gref, i:list factoryname, o:list prop, o:factory-name.
+main-mixin-requires Str GR GRFS [From|PO] SN :- !, std.do! [
+  main-factory-requires Str GR GRFS PO SN,
   % register factory
   PO => std.do! [
     coq.env.typeof GR (prod T TTy _),
@@ -1040,6 +1055,8 @@ main-declare-structure Module GRFS ClosureCheck :- std.do! [
   if-verbose (coq.say "HB: end modules; export" Exports),
 
   export Exports,
+
+  declare-factory-abbrev Module (factory-by-classname ClassName),
 ].
 
 pred main-begin-declare i:string, i:string, i:list gref, i:declaration.
@@ -1176,30 +1193,30 @@ main-declare-asset (asset-parameter Name T Rest as R) D :- std.do! [
   Ty = sort (typ U),
   coq.env.add-const Name _ Ty tt tt C, % no body, local -> a variable
   TheType = global (const C),
-  collect-asset-parameters (Rest TheType) [] TheType D
+  collect-asset-parameters (Rest TheType) [] Module TheType D
 ].
 
-pred collect-asset-parameters i:asset-decl, i:list factoryname, i:term, i:asset.
-collect-asset-parameters (asset-parameter _ T Rest) GRFS TheType D :- std.do! [
+pred collect-asset-parameters i:asset-decl, i:list factoryname, i:id, i:term, i:asset.
+collect-asset-parameters (asset-parameter _ T Rest) GRFS Module TheType D :- std.do! [
   std.assert! (T = app[global F, TheType]) "Factory not applied to the type variable",
   std.assert! (pi x y\ Rest x = Rest y) "Factories cannot be mentioned in the mixin",
   Dummy = sort prop,
-  collect-asset-parameters (Rest Dummy) [F|GRFS] TheType D
+  collect-asset-parameters (Rest Dummy) [F|GRFS] Module TheType D
 ].
 
-collect-asset-parameters (asset-alias _ Ty) GRFS TheType D :-
+collect-asset-parameters (asset-alias _ Ty) GRFS Module TheType D :-
   std.assert! (D = asset-factory) "Mixins cannot be aliases",
   % refresh implicit arguments, since many binders are now gone
   (pi X Y\ copy X Y :- var X, !) => copy Ty Ty1,
-  declare-factory-alias Ty1 GRFS TheType.
+  declare-factory-alias Ty1 GRFS Module TheType.
 
-collect-asset-parameters (asset-record _ Sort _ Fields) GRFS TheType D :-
+collect-asset-parameters (asset-record _ Sort _ Fields) GRFS Module TheType D :-
   % refresh implicit arguments, since many binders are now gone
   (pi X Y\ copy X Y :- var X, !) => (copy-fields Fields Fields0, copy Sort Sort1),
-  declare-mixin-or-factory Sort1 Fields0 GRFS TheType D.
+  declare-mixin-or-factory Sort1 Fields0 GRFS Module TheType D.
 
-pred declare-factory-alias i:term, i:list factoryname, i:term.
-declare-factory-alias Ty1 GRFS TheType :- std.do! [
+pred declare-factory-alias i:term, i:list factoryname, i:id, i:term.
+declare-factory-alias Ty1 GRFS Module TheType :- std.do! [
 
   main-declare-context TheType {std.rev GRFS} Hyps,
 
@@ -1223,7 +1240,7 @@ declare-factory-alias Ty1 GRFS TheType :- std.do! [
   mk-phant-abbrev "Axioms" PhGRK _ _,
 
   std.map Hyps mixin-src_mixin ML,
-  main-factory-requires "axioms" (const C) ML Props,
+  main-factory-requires "axioms" (const C) ML Props SN,
 
   if-verbose (coq.say "HB: start module Exports"),
 
@@ -1238,10 +1255,12 @@ declare-factory-alias Ty1 GRFS TheType :- std.do! [
   if-verbose (coq.say "HB: end modules and sections; export" Exports),
 
   export Exports,
+
+  declare-factory-abbrev Module SN,
 ].
 
-pred declare-mixin-or-factory i:term, i:record-decl, i:list factoryname, i:term, i:asset.
-declare-mixin-or-factory Sort1 Fields0 GRFS TheType D :- std.do! [
+pred declare-mixin-or-factory i:term, i:record-decl, i:list factoryname, i:id, i:term, i:asset.
+declare-mixin-or-factory Sort1 Fields0 GRFS Module TheType D :- std.do! [
   if (D = asset-mixin) (Fields1 = Fields0)
      (Fields1 = (field _ "_" {{ lib:hb.unify lp:TheType lp:TheType lib:hb.none }} _\ Fields0)),
   main-declare-context TheType {std.rev GRFS} Hyps,
@@ -1268,8 +1287,8 @@ declare-mixin-or-factory Sort1 Fields0 GRFS TheType D :- std.do! [
 
   std.map Hyps mixin-src_mixin ML,
   if (D = asset-mixin)
-     (main-mixin-requires "axioms" (indt R) ML Props)
-     (main-factory-requires "axioms" (indt R) ML Props),
+     (main-mixin-requires "axioms" (indt R) ML Props SN)
+     (main-factory-requires "axioms" (indt R) ML Props SN),
 
   if-verbose (coq.say "HB: start module Exports"),
 
@@ -1284,5 +1303,7 @@ declare-mixin-or-factory Sort1 Fields0 GRFS TheType D :- std.do! [
   if-verbose (coq.say "HB: end modules and sections; export" Exports),
 
   export Exports,
+
+  declare-factory-abbrev Module SN,
 ].
 
diff --git a/readme.v b/readme.v
index 0a2400640..bbf3e06ff 100644
--- a/readme.v
+++ b/readme.v
@@ -10,7 +10,7 @@ HB.mixin Record AddComoid_of_Type A := {
   add0r : forall x, add zero x = x;
 }.
 #[verbose]
-HB.structure Definition AddComoid := { A of AddComoid_of_Type.axioms A }.
+HB.structure Definition AddComoid := { A of AddComoid_of_Type A }.
 
 Notation "0" := zero.
 Infix "+" := add.
@@ -18,12 +18,12 @@ Infix "+" := add.
 Check forall (M : AddComoid.type) (x : M), x + x = 0.
 
 #[verbose]
-HB.mixin Record AbelianGrp_of_AddComoid A of AddComoid.axioms A := {
+HB.mixin Record AbelianGrp_of_AddComoid A of AddComoid A := {
   opp : A -> A;
   addNr : forall x, opp x + x = 0;
 }.
 #[verbose]
-HB.structure Definition AbelianGrp := { A of AbelianGrp_of_AddComoid.axioms A & }.
+HB.structure Definition AbelianGrp := { A of AbelianGrp_of_AddComoid A & }.
 
 Notation "- x" := (opp x).
 

From 606033aaef70fd7771357e089dd4a4e5e6693b41 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 11 Mar 2020 10:57:57 +0100
Subject: [PATCH 2/5] update all files wrt axioms

---
 demo1/hierarchy_0.v          |  2 +-
 demo1/hierarchy_1.v          |  8 +++---
 demo1/hierarchy_2.v          | 18 ++++++------
 demo1/hierarchy_3.v          | 24 ++++++++--------
 demo1/hierarchy_4.v          | 30 +++++++++----------
 demo1/hierarchy_5.v          | 40 +++++++++++++-------------
 demo2/stage10.v              | 16 +++++------
 demo2/stage11.v              | 56 ++++++++++++++++++------------------
 demo3/hierarchy_0.v          |  6 ++--
 demo3/hierarchy_1.v          | 12 ++++----
 demo3/hierarchy_2.v          | 20 ++++++-------
 structures.v                 | 24 ++++++++--------
 tests/duplicate_structure.v  |  4 +--
 tests/type_of_exported_ops.v |  2 +-
 14 files changed, 131 insertions(+), 131 deletions(-)

diff --git a/demo1/hierarchy_0.v b/demo1/hierarchy_0.v
index 73d1a2e40..c8cd4dbb3 100644
--- a/demo1/hierarchy_0.v
+++ b/demo1/hierarchy_0.v
@@ -23,7 +23,7 @@ HB.mixin Record Ring_of_TYPE A := {
   mulrDl : left_distributive mul add;
   mulrDr : right_distributive mul add;
 }.
-HB.structure Definition Ring := { A of Ring_of_TYPE.axioms A }.
+HB.structure Definition Ring := { A of Ring_of_TYPE A }.
 
 (* Notations *)
 
diff --git a/demo1/hierarchy_1.v b/demo1/hierarchy_1.v
index 3e2b7c832..af64196bd 100644
--- a/demo1/hierarchy_1.v
+++ b/demo1/hierarchy_1.v
@@ -16,9 +16,9 @@ HB.mixin Record AddComoid_of_TYPE A := {
   addrC : commutative add;
   add0r : left_id zero add;
 }.
-HB.structure Definition AddComoid := { A of AddComoid_of_TYPE.axioms A }.
+HB.structure Definition AddComoid := { A of AddComoid_of_TYPE A }.
 
-HB.mixin Record Ring_of_AddComoid A of AddComoid.axioms A := {
+HB.mixin Record Ring_of_AddComoid A of AddComoid A := {
   opp : A -> A;
   one : A;
   mul : A -> A -> A;
@@ -47,7 +47,7 @@ HB.factory Record Ring_of_TYPE A := {
   mulrDr : right_distributive mul add;
 }.
 
-HB.builders Context A (a : Ring_of_TYPE.axioms A).
+HB.builders Context A (a : Ring_of_TYPE A).
 
   Definition to_AddComoid_of_TYPE :=
     AddComoid_of_TYPE.Axioms A zero_a add_a addrA_a addrC_a add0r_a.
@@ -62,7 +62,7 @@ HB.end.
 
 (* End change *)
 
-HB.structure Definition Ring := { A of Ring_of_TYPE.axioms A }.
+HB.structure Definition Ring := { A of Ring_of_TYPE A }.
 
 (* Notations *)
 
diff --git a/demo1/hierarchy_2.v b/demo1/hierarchy_2.v
index 51b6b1ee6..d659b0d0c 100644
--- a/demo1/hierarchy_2.v
+++ b/demo1/hierarchy_2.v
@@ -14,11 +14,11 @@ HB.mixin Record AddComoid_of_TYPE A := {
   addrC : commutative add;
   add0r : left_id zero add;
 }.
-HB.structure Definition AddComoid := { A of AddComoid_of_TYPE.axioms A }.
+HB.structure Definition AddComoid := { A of AddComoid_of_TYPE A }.
 
 (* Begin change *)
 
-HB.mixin Record AddAG_of_AddComoid A of AddComoid.axioms A := {
+HB.mixin Record AddAG_of_AddComoid A of AddComoid A := {
   opp : A -> A;
   addNr : left_inverse zero opp add;
 }.
@@ -32,7 +32,7 @@ HB.factory Record AddAG_of_TYPE A := {
   addNr : left_inverse zero opp add;
 }.
 
-HB.builders Context A (a : AddAG_of_TYPE.axioms A).
+HB.builders Context A (a : AddAG_of_TYPE A).
 
   Definition to_AddComoid_of_TYPE :=
     AddComoid_of_TYPE.Axioms A zero_a add_a addrA_a addrC_a add0r_a.
@@ -43,9 +43,9 @@ HB.builders Context A (a : AddAG_of_TYPE.axioms A).
   HB.instance A to_AddAG_of_AddComoid.
 
 HB.end.
-HB.structure Definition AddAG := { A of AddAG_of_TYPE.axioms A }.
+HB.structure Definition AddAG := { A of AddAG_of_TYPE A }.
 
-HB.mixin Record Ring_of_AddAG A of AddAG.axioms A := {
+HB.mixin Record Ring_of_AddAG A of AddAG A := {
   one : A;
   mul : A -> A -> A;
   mulrA : associative mul;
@@ -54,7 +54,7 @@ HB.mixin Record Ring_of_AddAG A of AddAG.axioms A := {
   mulrDl : left_distributive mul add;
   mulrDr : right_distributive mul add;
 }.
-HB.factory Record Ring_of_AddComoid A of AddComoid.axioms A := {
+HB.factory Record Ring_of_AddComoid A of AddComoid A := {
   opp : A -> A;
   one : A;
   mul : A -> A -> A;
@@ -66,7 +66,7 @@ HB.factory Record Ring_of_AddComoid A of AddComoid.axioms A := {
   mulrDr : right_distributive mul add;
 }.
 
-HB.builders Context A (a : Ring_of_AddComoid.axioms A).
+HB.builders Context A (a : Ring_of_AddComoid A).
 
   Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Axioms A _ addNr_a.
   HB.instance A to_AddAG_of_AddComoid.
@@ -96,7 +96,7 @@ HB.factory Record Ring_of_TYPE A := {
   mulrDr : right_distributive mul add;
 }.
 
-HB.builders Context A (a : Ring_of_TYPE.axioms A).
+HB.builders Context A (a : Ring_of_TYPE A).
 
   Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Axioms A
     zero_a add_a addrA_a addrC_a add0r_a.
@@ -107,7 +107,7 @@ HB.builders Context A (a : Ring_of_TYPE.axioms A).
   HB.instance A to_Ring_of_AddComoid.
 HB.end.
 
-HB.structure Definition Ring := { A of Ring_of_TYPE.axioms A }.
+HB.structure Definition Ring := { A of Ring_of_TYPE A }.
 
 (* Notations *)
 
diff --git a/demo1/hierarchy_3.v b/demo1/hierarchy_3.v
index 6cef3f76f..07d11a3c6 100644
--- a/demo1/hierarchy_3.v
+++ b/demo1/hierarchy_3.v
@@ -16,9 +16,9 @@ HB.mixin Record AddComoid_of_TYPE A := {
   addrC : commutative add;
   add0r : left_id zero add;
 }.
-HB.structure Definition AddComoid := { A of AddComoid_of_TYPE.axioms A }.
+HB.structure Definition AddComoid := { A of AddComoid_of_TYPE A }.
 
-HB.mixin Record AddAG_of_AddComoid A of AddComoid.axioms A := {
+HB.mixin Record AddAG_of_AddComoid A of AddComoid A := {
   opp : A -> A;
   addNr : left_inverse zero opp add;
 }.
@@ -32,7 +32,7 @@ HB.factory Record AddAG_of_TYPE A := {
   addNr : left_inverse zero opp add;
 }.
 
-HB.builders Context A (a : AddAG_of_TYPE.axioms A).
+HB.builders Context A (a : AddAG_of_TYPE A).
 
   Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Axioms A
     zero_a add_a addrA_a addrC_a add0r_a.
@@ -41,11 +41,11 @@ HB.builders Context A (a : AddAG_of_TYPE.axioms A).
   Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Axioms A _ addNr_a.
   HB.instance A to_AddAG_of_AddComoid.
 HB.end.
-HB.structure Definition AddAG := { A of AddAG_of_TYPE.axioms A }.
+HB.structure Definition AddAG := { A of AddAG_of_TYPE A }.
 
 (* Begin change *)
 
-HB.mixin Record SemiRing_of_AddComoid A of AddComoid.axioms A := {
+HB.mixin Record SemiRing_of_AddComoid A of AddComoid A := {
   one : A;
   mul : A -> A -> A;
   mulrA : associative mul;
@@ -56,9 +56,9 @@ HB.mixin Record SemiRing_of_AddComoid A of AddComoid.axioms A := {
   mul0r : left_zero zero mul;
   mulr0 : right_zero zero mul;
 }.
-HB.structure Definition SemiRing := { A of AddComoid.axioms A & SemiRing_of_AddComoid.axioms A }.
+HB.structure Definition SemiRing := { A of AddComoid A & SemiRing_of_AddComoid A }.
 
-HB.factory Record Ring_of_AddAG A of AddAG.axioms A := {
+HB.factory Record Ring_of_AddAG A of AddAG A := {
   one : A;
   mul : A -> A -> A;
   mulrA : associative mul;
@@ -68,7 +68,7 @@ HB.factory Record Ring_of_AddAG A of AddAG.axioms A := {
   mulrDr : right_distributive mul add;
 }.
 
-HB.builders Context A (a : Ring_of_AddAG.axioms A).
+HB.builders Context A (a : Ring_of_AddAG A).
 
   Fact mul0r : left_zero zero mul_a.
   Proof.
@@ -92,7 +92,7 @@ HB.builders Context A (a : Ring_of_AddAG.axioms A).
 HB.end.
 
 (* End change *)
-HB.factory Record Ring_of_AddComoid A of AddComoid.axioms A := {
+HB.factory Record Ring_of_AddComoid A of AddComoid A := {
   opp : A -> A;
   one : A;
   mul : A -> A -> A;
@@ -104,7 +104,7 @@ HB.factory Record Ring_of_AddComoid A of AddComoid.axioms A := {
   mulrDr : right_distributive mul add;
 }.
 
-HB.builders Context A (a : Ring_of_AddComoid.axioms A).
+HB.builders Context A (a : Ring_of_AddComoid A).
 
   Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Axioms A _ addNr_a.
   HB.instance A to_AddAG_of_AddComoid.
@@ -134,7 +134,7 @@ HB.factory Record Ring_of_TYPE A := {
   mulrDr : right_distributive mul add;
 }.
 
-HB.builders Context A (a : Ring_of_TYPE.axioms A).
+HB.builders Context A (a : Ring_of_TYPE A).
 
   Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Axioms A
     zero_a add_a addrA_a addrC_a add0r_a.
@@ -145,7 +145,7 @@ HB.builders Context A (a : Ring_of_TYPE.axioms A).
   HB.instance A to_Ring_of_AddComoid.
 HB.end.
 
-HB.structure Definition Ring := { A of Ring_of_TYPE.axioms A }.
+HB.structure Definition Ring := { A of Ring_of_TYPE A }.
 
 (* Notations *)
 
diff --git a/demo1/hierarchy_4.v b/demo1/hierarchy_4.v
index ebeb7c1ef..d2dd58946 100644
--- a/demo1/hierarchy_4.v
+++ b/demo1/hierarchy_4.v
@@ -17,9 +17,9 @@ HB.mixin Record AddMonoid_of_TYPE S := {
   add0r : left_id zero add;
   addr0 : right_id zero add;
 }.
-HB.structure Definition AddMonoid := { A of AddMonoid_of_TYPE.axioms A }.
+HB.structure Definition AddMonoid := { A of AddMonoid_of_TYPE A }.
 
-HB.mixin Record AddComoid_of_AddMonoid A of AddMonoid.axioms A := {
+HB.mixin Record AddComoid_of_AddMonoid A of AddMonoid A := {
   addrC : commutative (add : A -> A -> A);
 }.
 HB.factory Record AddComoid_of_TYPE A := {
@@ -30,7 +30,7 @@ HB.factory Record AddComoid_of_TYPE A := {
   add0r : left_id zero add;
 }.
 
-HB.builders Context A (a : AddComoid_of_TYPE.axioms A).
+HB.builders Context A (a : AddComoid_of_TYPE A).
 
   Fact addr0 : right_id zero_a add_a.
   Proof. by move=> x; rewrite addrC_a add0r_a. Qed.
@@ -43,11 +43,11 @@ HB.builders Context A (a : AddComoid_of_TYPE.axioms A).
     AddComoid_of_AddMonoid.Axioms A addrC_a.
   HB.instance A to_AddComoid_of_AddMonoid.
 HB.end.
-HB.structure Definition AddComoid := { A of AddComoid_of_TYPE.axioms A }.
+HB.structure Definition AddComoid := { A of AddComoid_of_TYPE A }.
 
 (* End change *)
 
-HB.mixin Record AddAG_of_AddComoid A of AddComoid.axioms A := {
+HB.mixin Record AddAG_of_AddComoid A of AddComoid A := {
   opp : A -> A;
   addNr : left_inverse zero opp add;
 }.
@@ -61,7 +61,7 @@ HB.factory Record AddAG_of_TYPE A := {
   addNr : left_inverse zero opp add;
 }.
 
-HB.builders Context A (a : AddAG_of_TYPE.axioms A).
+HB.builders Context A (a : AddAG_of_TYPE A).
 
   Definition to_AddComoid_of_TYPE :=
     AddComoid_of_TYPE.Axioms A zero_a add_a addrA_a addrC_a add0r_a.
@@ -71,9 +71,9 @@ HB.builders Context A (a : AddAG_of_TYPE.axioms A).
     AddAG_of_AddComoid.Axioms A _ addNr_a.
   HB.instance A to_AddAG_of_AddComoid.
 HB.end.
-HB.structure Definition AddAG := { A of AddAG_of_TYPE.axioms A }.
+HB.structure Definition AddAG := { A of AddAG_of_TYPE A }.
 
-HB.mixin Record SemiRing_of_AddComoid A of AddComoid.axioms A := {
+HB.mixin Record SemiRing_of_AddComoid A of AddComoid A := {
   one : A;
   mul : A -> A -> A;
   mulrA : associative mul;
@@ -84,9 +84,9 @@ HB.mixin Record SemiRing_of_AddComoid A of AddComoid.axioms A := {
   mul0r : left_zero zero mul;
   mulr0 : right_zero zero mul;
 }.
-HB.structure Definition SemiRing := { A of AddComoid.axioms A & SemiRing_of_AddComoid.axioms A }.
+HB.structure Definition SemiRing := { A of AddComoid A & SemiRing_of_AddComoid A }.
 
-HB.factory Record Ring_of_AddAG A of AddAG.axioms A := {
+HB.factory Record Ring_of_AddAG A of AddAG A := {
   one : A;
   mul : A -> A -> A;
   mulrA : associative mul;
@@ -96,7 +96,7 @@ HB.factory Record Ring_of_AddAG A of AddAG.axioms A := {
   mulrDr : right_distributive mul add;
 }.
 
-HB.builders Context A (a : Ring_of_AddAG.axioms A).
+HB.builders Context A (a : Ring_of_AddAG A).
 
   Fact mul0r : left_zero zero mul_a.
   Proof.
@@ -119,7 +119,7 @@ HB.builders Context A (a : Ring_of_AddAG.axioms A).
 HB.end.
 
 (* End change *)
-HB.factory Record Ring_of_AddComoid A of AddComoid.axioms A := {
+HB.factory Record Ring_of_AddComoid A of AddComoid A := {
   opp : A -> A;
   one : A;
   mul : A -> A -> A;
@@ -131,7 +131,7 @@ HB.factory Record Ring_of_AddComoid A of AddComoid.axioms A := {
   mulrDr : right_distributive mul add;
 }.
 
-HB.builders Context A (a : Ring_of_AddComoid.axioms A).
+HB.builders Context A (a : Ring_of_AddComoid A).
 
   Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Axioms A _ addNr_a.
   HB.instance A to_AddAG_of_AddComoid.
@@ -161,7 +161,7 @@ HB.factory Record Ring_of_TYPE A := {
   mulrDr : right_distributive mul add;
 }.
 
-HB.builders Context A (a : Ring_of_TYPE.axioms A).
+HB.builders Context A (a : Ring_of_TYPE A).
 
   Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Axioms A
     zero_a add_a addrA_a addrC_a add0r_a.
@@ -172,7 +172,7 @@ HB.builders Context A (a : Ring_of_TYPE.axioms A).
   HB.instance A to_Ring_of_AddComoid.
 HB.end.
 
-HB.structure Definition Ring := { A of Ring_of_TYPE.axioms A }.
+HB.structure Definition Ring := { A of Ring_of_TYPE A }.
 
 (* Notations *)
 
diff --git a/demo1/hierarchy_5.v b/demo1/hierarchy_5.v
index 32bf8fe56..5b86451fd 100644
--- a/demo1/hierarchy_5.v
+++ b/demo1/hierarchy_5.v
@@ -16,9 +16,9 @@ HB.mixin Record AddMonoid_of_TYPE S := {
   add0r : left_id zero add;
   addr0 : right_id zero add;
 }.
-HB.structure Definition AddMonoid := { A of AddMonoid_of_TYPE.axioms A }.
+HB.structure Definition AddMonoid := { A of AddMonoid_of_TYPE A }.
 
-HB.mixin Record AddComoid_of_AddMonoid A of AddMonoid.axioms A := {
+HB.mixin Record AddComoid_of_AddMonoid A of AddMonoid A := {
   addrC : commutative (add : A -> A -> A);
 }.
 HB.factory Record AddComoid_of_TYPE A := {
@@ -29,7 +29,7 @@ HB.factory Record AddComoid_of_TYPE A := {
   add0r : left_id zero add;
 }.
 
-HB.builders Context A (a : AddComoid_of_TYPE.axioms A).
+HB.builders Context A (a : AddComoid_of_TYPE A).
 
   Fact addr0 : right_id zero_a add_a.
   Proof. by move=> x; rewrite addrC_a add0r_a. Qed.
@@ -42,11 +42,11 @@ HB.builders Context A (a : AddComoid_of_TYPE.axioms A).
     AddComoid_of_AddMonoid.Axioms A addrC_a.
   HB.instance A to_AddComoid_of_AddMonoid.
 HB.end.
-HB.structure Definition AddComoid := { A of AddComoid_of_TYPE.axioms A }.
+HB.structure Definition AddComoid := { A of AddComoid_of_TYPE A }.
 
 (* End change *)
 
-HB.mixin Record AddAG_of_AddComoid A of AddComoid.axioms A := {
+HB.mixin Record AddAG_of_AddComoid A of AddComoid A := {
   opp : A -> A;
   addNr : left_inverse zero opp add;
 }.
@@ -60,7 +60,7 @@ HB.factory Record AddAG_of_TYPE A := {
   addNr : left_inverse zero opp add;
 }.
 
-HB.builders Context A (a : AddAG_of_TYPE.axioms A).
+HB.builders Context A (a : AddAG_of_TYPE A).
 
   Definition to_AddComoid_of_TYPE :=
     AddComoid_of_TYPE.Axioms A zero_a add_a addrA_a addrC_a add0r_a.
@@ -70,11 +70,11 @@ HB.builders Context A (a : AddAG_of_TYPE.axioms A).
     AddAG_of_AddComoid.Axioms A _ addNr_a.
   HB.instance A to_AddAG_of_AddComoid.
 HB.end.
-HB.structure Definition AddAG := { A of AddAG_of_TYPE.axioms A }.
+HB.structure Definition AddAG := { A of AddAG_of_TYPE A }.
 
 (* Begin changes *)
 
-HB.mixin Record BiNearRing_of_AddMonoid A of AddMonoid.axioms A := {
+HB.mixin Record BiNearRing_of_AddMonoid A of AddMonoid A := {
   one : A;
   mul : A -> A -> A;
   mulrA : associative mul;
@@ -85,23 +85,23 @@ HB.mixin Record BiNearRing_of_AddMonoid A of AddMonoid.axioms A := {
   mul0r : left_zero zero mul;
   mulr0 : right_zero zero mul;
 }.
-HB.structure Definition BiNearRing := { A of AddMonoid.axioms A & BiNearRing_of_AddMonoid.axioms A }.
+HB.structure Definition BiNearRing := { A of AddMonoid A & BiNearRing_of_AddMonoid A }.
 
 (* this factory is accidentally a duplicate of BiNearRing_of_AddMonoid *)
 (* we alias it for backward compatilibity and uniformity purposes *)
-HB.factory Definition SemiRing_of_AddComoid A of AddComoid.axioms A :=
-    BiNearRing_of_AddMonoid.axioms A.
-HB.builders Context A (a : SemiRing_of_AddComoid.axioms A).
+HB.factory Definition SemiRing_of_AddComoid A of AddComoid A :=
+    BiNearRing_of_AddMonoid A.
+HB.builders Context A (a : SemiRing_of_AddComoid A).
 
-  Definition to_BiNearRing_of_AddMonoid : BiNearRing_of_AddMonoid.axioms A := a.
+  Definition to_BiNearRing_of_AddMonoid : BiNearRing_of_AddMonoid A := a.
   HB.instance A to_BiNearRing_of_AddMonoid.
 HB.end.
 
 (* End changes *)
 
-HB.structure Definition SemiRing := { A of AddComoid.axioms A & SemiRing_of_AddComoid.axioms A }.
+HB.structure Definition SemiRing := { A of AddComoid A & SemiRing_of_AddComoid A }.
 
-HB.factory Record Ring_of_AddAG A of AddAG.axioms A := {
+HB.factory Record Ring_of_AddAG A of AddAG A := {
   one : A;
   mul : A -> A -> A;
   mulrA : associative mul;
@@ -111,7 +111,7 @@ HB.factory Record Ring_of_AddAG A of AddAG.axioms A := {
   mulrDr : right_distributive mul add;
 }.
 
-HB.builders Context A (a : Ring_of_AddAG.axioms A).
+HB.builders Context A (a : Ring_of_AddAG A).
 
   Fact mul0r : left_zero zero mul_a.
   Proof.
@@ -133,7 +133,7 @@ HB.builders Context A (a : Ring_of_AddAG.axioms A).
 
 HB.end.
 
-HB.factory Record Ring_of_AddComoid A of AddComoid.axioms A := {
+HB.factory Record Ring_of_AddComoid A of AddComoid A := {
   opp : A -> A;
   one : A;
   mul : A -> A -> A;
@@ -145,7 +145,7 @@ HB.factory Record Ring_of_AddComoid A of AddComoid.axioms A := {
   mulrDr : right_distributive mul add;
 }.
 
-HB.builders Context A (a :Ring_of_AddComoid.axioms A).
+HB.builders Context A (a :Ring_of_AddComoid A).
 
   Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Axioms A _ addNr_a.
   HB.instance A to_AddAG_of_AddComoid.
@@ -173,7 +173,7 @@ HB.factory Record Ring_of_TYPE A := {
   mulrDr : right_distributive mul add;
 }.
 
-HB.builders Context A (a : Ring_of_TYPE.axioms A).
+HB.builders Context A (a : Ring_of_TYPE A).
 
   Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Axioms A
     zero_a add_a addrA_a addrC_a add0r_a.
@@ -184,7 +184,7 @@ HB.builders Context A (a : Ring_of_TYPE.axioms A).
   HB.instance A to_Ring_of_AddComoid.
 HB.end.
 
-HB.structure Definition Ring := { A of Ring_of_TYPE.axioms A }.
+HB.structure Definition Ring := { A of Ring_of_TYPE A }.
 
 (* Notations *)
 
diff --git a/demo2/stage10.v b/demo2/stage10.v
index b30cc8dff..617302c9e 100644
--- a/demo2/stage10.v
+++ b/demo2/stage10.v
@@ -21,7 +21,7 @@ HB.mixin Record AddAG_of_TYPE A := {
   add0r : left_id zero add;
   addNr : left_inverse zero opp add;
 }.
-HB.structure Definition AddAG := { A of AddAG_of_TYPE.axioms A }.
+HB.structure Definition AddAG := { A of AddAG_of_TYPE A }.
 
 Notation "0" := zero : hb_scope.
 Infix "+" := (@add _) : hb_scope.
@@ -78,7 +78,7 @@ Proof. by rewrite opprD opprK addrC. Qed.
 
 End AddAGTheory.
 
-HB.mixin Record Ring_of_AddAG A of AddAG.axioms A := {
+HB.mixin Record Ring_of_AddAG A of AddAG A := {
   one : A;
   mul : A -> A -> A;
   mulrA : associative mul;
@@ -104,7 +104,7 @@ HB.factory Record Ring_of_TYPE A := {
   mulrDr : right_distributive mul add;
 }.
 
-HB.builders Context A (a : Ring_of_TYPE.axioms A).
+HB.builders Context A (a : Ring_of_TYPE A).
 
 Definition to_AddAG_of_TYPE := AddAG_of_TYPE.Axioms A
     _ _ _ addrA_a addrC_a add0r_a addNr_a.
@@ -115,7 +115,7 @@ Definition to_AddAG_of_TYPE := AddAG_of_TYPE.Axioms A
   HB.instance A to_Ring_of_AddAG.
 HB.end.
 
-HB.structure Definition Ring := { A of Ring_of_TYPE.axioms A }.
+HB.structure Definition Ring := { A of Ring_of_TYPE A }.
 
 Notation "1" := one : hb_scope.
 Infix "*" := (@mul _) : hb_scope.
@@ -127,7 +127,7 @@ HB.mixin Record Topological T := {
     (forall i, D i -> open (F i)) -> open (\bigcup_(i in D) F i);
   open_setI : forall X Y : set T, open X -> open Y -> open (setI X Y);
 }.
-HB.structure Definition TopologicalSpace := { A of Topological.axioms A }.
+HB.structure Definition TopologicalSpace := { A of Topological A }.
 
 Hint Extern 0 (open setT) => now apply: open_setT : core.
 
@@ -138,7 +138,7 @@ HB.factory Record TopologicalBase T := {
     forall z, (X `&` Y) z -> exists2 Z, open_base Z & Z z /\ Z `<=` X `&` Y
 }.
 
-HB.builders Context T (a : TopologicalBase.axioms T).
+HB.builders Context T (a : TopologicalBase T).
 
   Definition open_of : (T -> Prop) -> Prop :=
     [set A | exists2 D, D `<=` open_base_a & A = \bigcup_(X in D) X].
@@ -200,12 +200,12 @@ Definition continuous {T T' : TopologicalSpace.type} (f : T -> T') :=
 Definition continuous2 {T T' T'': TopologicalSpace.type}
   (f : T -> T' -> T'') := continuous (fun xy => f xy.1 xy.2).
 
-HB.mixin Record JoinTAddAG T of AddAG_of_TYPE.axioms T & Topological.axioms T := {
+HB.mixin Record JoinTAddAG T of AddAG_of_TYPE T & Topological T := {
   add_continuous : continuous2 (add : T -> T -> T);
   opp_continuous : continuous (opp : T -> T)
 }.
 
-HB.structure Definition TAddAG := { A of Topological.axioms A & AddAG_of_TYPE.axioms A & JoinTAddAG.axioms A }.
+HB.structure Definition TAddAG := { A of Topological A & AddAG_of_TYPE A & JoinTAddAG A }.
 
 (* Instance *)
 
diff --git a/demo2/stage11.v b/demo2/stage11.v
index 97a6344a8..fef321af6 100644
--- a/demo2/stage11.v
+++ b/demo2/stage11.v
@@ -21,7 +21,7 @@ HB.mixin Record AddAG_of_TYPE A := {
   add0r : left_id zero add;
   addNr : left_inverse zero opp add;
 }.
-HB.structure Definition AddAG := { A of AddAG_of_TYPE.axioms A }.
+HB.structure Definition AddAG := { A of AddAG_of_TYPE A }.
 
 (* TODO: command hb.module_export which creates a module,
    exports it immediatly and remembers that it should be
@@ -82,7 +82,7 @@ Proof. by rewrite opprD opprK addrC. Qed.
 
 End AddAGTheory.
 
-HB.mixin Record Ring_of_AddAG A of AddAG.axioms A := {
+HB.mixin Record Ring_of_AddAG A of AddAG A := {
   one : A;
   mul : A -> A -> A;
   mulrA : associative mul;
@@ -108,7 +108,7 @@ HB.factory Record Ring_of_TYPE A := {
   mulrDr : right_distributive mul add;
 }.
 
-HB.builders Context A (a : Ring_of_TYPE.axioms A).
+HB.builders Context A (a : Ring_of_TYPE A).
 
   Definition to_AddAG := AddAG_of_TYPE.Axioms A
     _ _ _ addrA_a addrC_a add0r_a addNr_a.
@@ -119,7 +119,7 @@ HB.builders Context A (a : Ring_of_TYPE.axioms A).
   HB.instance A to_Ring.
 HB.end.
 
-HB.structure Definition Ring := { A of Ring_of_TYPE.axioms A }.
+HB.structure Definition Ring := { A of Ring_of_TYPE A }.
 
 Notation "1" := one : hb_scope.
 Infix "*" := (@mul _) : hb_scope.
@@ -131,7 +131,7 @@ HB.mixin Record Topological T := {
   (forall i, D i -> open (F i)) -> open (\bigcup_(i in D) F i);
   open_setI : forall X Y : set T, open X -> open Y -> open (setI X Y);
 }.
-HB.structure Definition TopologicalSpace := { A of Topological.axioms A }.
+HB.structure Definition TopologicalSpace := { A of Topological A }.
 
 Hint Extern 0 (open setT) => now apply: open_setT : core.
 
@@ -142,7 +142,7 @@ HB.factory Record TopologicalBase T := {
     forall z, (X `&` Y) z -> exists2 Z, open_base Z & Z z /\ Z `<=` X `&` Y
 }.
 
-HB.builders Context T (a : TopologicalBase.axioms T).
+HB.builders Context T (a : TopologicalBase T).
 
   Definition open_of :=
     [set A | exists2 D, D `<=` open_base_a & A = \bigcup_(X in D) X].
@@ -208,13 +208,13 @@ Definition continuous {T T' : TopologicalSpace.type} (f : T -> T') :=
 Definition continuous2 {T T' T'': TopologicalSpace.type}
   (f : T -> T' -> T'') := continuous (fun xy => f xy.1 xy.2).
 
-HB.mixin Record JoinTAddAG_wo_Uniform T of AddAG_of_TYPE.axioms T & Topological.axioms T := {
+HB.mixin Record JoinTAddAG_wo_Uniform T of AddAG_of_TYPE T & Topological T := {
   add_continuous : continuous2 (add : T -> T -> T);
   opp_continuous : continuous (opp : T -> T)
 }.
 
 HB.structure Definition TAddAG_wo_Uniform :=
-  { A of Topological.axioms A & AddAG_of_TYPE.axioms A & JoinTAddAG_wo_Uniform.axioms A }.
+  { A of Topological A & AddAG_of_TYPE A & JoinTAddAG_wo_Uniform A }.
 
 HB.mixin Record Uniform_wo_Topology U := {
   entourage : set (set (U * U)) ;
@@ -224,7 +224,7 @@ HB.mixin Record Uniform_wo_Topology U := {
   entourage_split : forall A, entourage A ->
     exists2 B, entourage B & graph_comp B B `<=` A ;
 }.
-HB.structure Definition UniformSpace_wo_Topology := { A of Uniform_wo_Topology.axioms A }.
+HB.structure Definition UniformSpace_wo_Topology := { A of Uniform_wo_Topology A }.
 
 (* TODO: have a command hb.typealias which register "typealias factories"
    which turn a typealias into factories *)
@@ -247,21 +247,21 @@ Section Uniform_Topology.
 
 End Uniform_Topology.
 
-HB.mixin Record Join_Uniform_Topology U of Topological.axioms U & Uniform_wo_Topology.axioms U := {
+HB.mixin Record Join_Uniform_Topology U of Topological U & Uniform_wo_Topology U := {
   openE : open = (uniform_open _ : set (set (uniform U)))
 }.
 
 (* TODO: this factory should be replaced by type alias uniform *)
-HB.factory Record Uniform_Topology U of Uniform_wo_Topology.axioms U := { }.
+HB.factory Record Uniform_Topology U of Uniform_wo_Topology U := { }.
 
-HB.builders Context U (f : Uniform_Topology.axioms U).
-  Definition to_Topological : Topological.axioms U := (uniform_topology _).
+HB.builders Context U (f : Uniform_Topology U).
+  Definition to_Topological : Topological U := (uniform_topology _).
   HB.instance U to_Topological.
 HB.end.
 
 HB.structure Definition UniformSpace := { A of
-   Uniform_Topology.axioms A    (* should be replaced by typealias uniform *)
-   & Uniform_wo_Topology.axioms A }. (* TODO: should be ommited                 *)
+   Uniform_Topology A    (* should be replaced by typealias uniform *)
+   & Uniform_wo_Topology A }. (* TODO: should be ommited                 *)
 
 (* TODO: this is another typealias *)
 Definition TAddAG (T : Type) := T.
@@ -289,7 +289,7 @@ Section TAddAGUniform.
   Lemma TAddAG_uniform_topologyE :
      open = (uniform_open _ : set (set (uniform TT))).
   Admitted.
-  Definition TAddAG_Join_Uniform_Topology : Join_Uniform_Topology.axioms (TAddAG T)
+  Definition TAddAG_Join_Uniform_Topology : Join_Uniform_Topology (TAddAG T)
     := Join_Uniform_Topology.Axioms _ TAddAG_uniform_topologyE.
   HB.instance (TAddAG (TAddAG_wo_Uniform.sort T))
     TAddAG_Join_Uniform_Topology.
@@ -301,20 +301,20 @@ Section TAddAGUniform.
 End TAddAGUniform.
 
 HB.structure Definition Uniform_TAddAG_unjoined :=
-  { A of TAddAG_wo_Uniform.axioms A & Uniform_wo_Topology.axioms A }.
+  { A of TAddAG_wo_Uniform A & Uniform_wo_Topology A }.
   (* should be created automatically *)
-HB.mixin Record Join_TAddAG_Uniform T of Uniform_TAddAG_unjoined.axioms T := {
+HB.mixin Record Join_TAddAG_Uniform T of Uniform_TAddAG_unjoined T := {
     entourageE :
     entourage = (TAddAG_entourage _ : set (set (TAddAG T * TAddAG T)))
 }.
 
   (* TODO: should be subsumed by the type alias TAddAG *)
-HB.factory Record TAddAG_Uniform U of TAddAG_wo_Uniform.axioms U := { }.
+HB.factory Record TAddAG_Uniform U of TAddAG_wo_Uniform U := { }.
 
-HB.builders Context U of TAddAG_Uniform.axioms U.
-  Definition to_Uniform_wo_Topology : Uniform_wo_Topology.axioms U := (TAddAG_uniform _).
+HB.builders Context U of TAddAG_Uniform U.
+  Definition to_Uniform_wo_Topology : Uniform_wo_Topology U := (TAddAG_uniform _).
   HB.instance U to_Uniform_wo_Topology.
-  Definition to_Join_Uniform_Topology : Join_Uniform_Topology.axioms U :=
+  Definition to_Join_Uniform_Topology : Join_Uniform_Topology U :=
     (TAddAG_Join_Uniform_Topology _).
   HB.instance U to_Join_Uniform_Topology.
   Definition to_Join_TAddAG_Uniform :=
@@ -323,14 +323,14 @@ HB.builders Context U of TAddAG_Uniform.axioms U.
 HB.end.
 
 HB.structure Definition TAddAG :=
-   { A of TAddAG_Uniform.axioms A (* TODO: should be replaced by type alias TAddAG *)
-        & TAddAG_wo_Uniform.axioms A }. (* TODO: should be omitted *)
+   { A of TAddAG_Uniform A (* TODO: should be replaced by type alias TAddAG *)
+        & TAddAG_wo_Uniform A }. (* TODO: should be omitted *)
 
-HB.factory Definition JoinTAddAG T of AddAG_of_TYPE.axioms T & Topological.axioms T :=
-  (JoinTAddAG_wo_Uniform.axioms T).
+HB.factory Definition JoinTAddAG T of AddAG_of_TYPE T & Topological T :=
+  (JoinTAddAG_wo_Uniform T).
 
-HB.builders Context T (a : JoinTAddAG.axioms T).
-  Definition to_JoinTAddAG_wo_Uniform : JoinTAddAG_wo_Uniform.axioms T := a.
+HB.builders Context T (a : JoinTAddAG T).
+  Definition to_JoinTAddAG_wo_Uniform : JoinTAddAG_wo_Uniform T := a.
   HB.instance T to_JoinTAddAG_wo_Uniform.
   (* TODO: Nice error message when factory builders do not depend on the source factory 'a'*)
   Definition to_Uniform := let _ := a in TAddAG_Uniform.Axioms T.
diff --git a/demo3/hierarchy_0.v b/demo3/hierarchy_0.v
index fdbe4a5ea..0550bb812 100644
--- a/demo3/hierarchy_0.v
+++ b/demo3/hierarchy_0.v
@@ -8,9 +8,9 @@ HB.mixin Record MulMonoid_of_Type A := {
   mul1r : left_id one mul;
   mulr1 : right_id one mul;
 }.
-HB.structure Definition MulMonoid := { A of MulMonoid_of_Type.axioms A }.
+HB.structure Definition MulMonoid := { A of MulMonoid_of_Type A }.
 
-HB.mixin Record Ring_of_MulMonoid A of MulMonoid.axioms A := {
+HB.mixin Record Ring_of_MulMonoid A of MulMonoid A := {
   zero : A;
   add : A -> A -> A;
   addrA : associative add;
@@ -22,5 +22,5 @@ HB.mixin Record Ring_of_MulMonoid A of MulMonoid.axioms A := {
   mulrDl : left_distributive mul add;
   mulrDr : right_distributive mul add;
 }.
-HB.structure Definition Ring := { A of MulMonoid.axioms A & Ring_of_MulMonoid.axioms A }.
+HB.structure Definition Ring := { A of MulMonoid A & Ring_of_MulMonoid A }.
 
diff --git a/demo3/hierarchy_1.v b/demo3/hierarchy_1.v
index df756f410..fc31b38b8 100644
--- a/demo3/hierarchy_1.v
+++ b/demo3/hierarchy_1.v
@@ -8,7 +8,7 @@ HB.mixin Record MulMonoid_of_Type A := {
   mul1r : left_id one mul;
   mulr1 : right_id one mul;
 }.
-HB.structure Definition MulMonoid := { A of MulMonoid_of_Type.axioms A }.
+HB.structure Definition MulMonoid := { A of MulMonoid_of_Type A }.
 
 HB.mixin Record AddMonoid_of_Type A := {
   zero : A;
@@ -17,18 +17,18 @@ HB.mixin Record AddMonoid_of_Type A := {
   add0r : left_id zero add;
   addr0 : right_id zero add;
 }.
-HB.structure Definition AddMonoid := { A of AddMonoid_of_Type.axioms A }.
+HB.structure Definition AddMonoid := { A of AddMonoid_of_Type A }.
 
-HB.mixin Record Ring_of_AddMulMonoid A of MulMonoid.axioms A & AddMonoid.axioms A := {
+HB.mixin Record Ring_of_AddMulMonoid A of MulMonoid A & AddMonoid A := {
   opp : A -> A;
   addrC : commutative (add : A -> A -> A);
   addNr : left_inverse zero opp add;
   mulrDl : left_distributive mul (add : A -> A -> A);
   mulrDr : right_distributive mul (add : A -> A -> A);
 }.
-HB.structure Definition Ring := { A of MulMonoid.axioms A & AddMonoid.axioms A & Ring_of_AddMulMonoid.axioms A }.
+HB.structure Definition Ring := { A of MulMonoid A & AddMonoid A & Ring_of_AddMulMonoid A }.
 
-HB.factory Record Ring_of_MulMonoid A of MulMonoid.axioms A := {
+HB.factory Record Ring_of_MulMonoid A of MulMonoid A := {
   zero : A;
   add : A -> A -> A;
   addrA : associative add;
@@ -41,7 +41,7 @@ HB.factory Record Ring_of_MulMonoid A of MulMonoid.axioms A := {
   mulrDr : right_distributive mul add;
 }.
 
-HB.builders Context A (a : Ring_of_MulMonoid.axioms A).
+HB.builders Context A (a : Ring_of_MulMonoid A).
 
   Definition to_AddMonoid_of_Type :=
     AddMonoid_of_Type.Axioms A zero_a add_a addrA_a add0r_a addr0_a.
diff --git a/demo3/hierarchy_2.v b/demo3/hierarchy_2.v
index 74011425f..b78951fc5 100644
--- a/demo3/hierarchy_2.v
+++ b/demo3/hierarchy_2.v
@@ -8,7 +8,7 @@ HB.mixin Record MulMonoid_of_Type A := {
   mul1r : left_id one mul;
   mulr1 : right_id one mul;
 }.
-HB.structure Definition MulMonoid := { A of MulMonoid_of_Type.axioms A }.
+HB.structure Definition MulMonoid := { A of MulMonoid_of_Type A }.
 
 HB.mixin Record AddMonoid_of_Type A := {
   zero : A;
@@ -17,22 +17,22 @@ HB.mixin Record AddMonoid_of_Type A := {
   add0r : left_id zero add;
   addr0 : right_id zero add;
 }.
-HB.structure Definition AddMonoid := { A of AddMonoid_of_Type.axioms A }.
+HB.structure Definition AddMonoid := { A of AddMonoid_of_Type A }.
 
-HB.mixin Record AbGroup_of_AddMonoid A of AddMonoid.axioms A := {
+HB.mixin Record AbGroup_of_AddMonoid A of AddMonoid A := {
   opp : A -> A;
   addrC : commutative (add : A -> A -> A);
   addNr : left_inverse zero opp add;
 }.
-HB.structure Definition AbGroup := { A of AddMonoid.axioms A & AbGroup_of_AddMonoid.axioms A }.
+HB.structure Definition AbGroup := { A of AddMonoid A & AbGroup_of_AddMonoid A }.
 
-HB.mixin Record Ring_of_AbGroupMulMonoid A of MulMonoid.axioms A & AbGroup.axioms A := {
+HB.mixin Record Ring_of_AbGroupMulMonoid A of MulMonoid A & AbGroup A := {
   mulrDl : left_distributive mul (add : A -> A -> A);
   mulrDr : right_distributive mul (add : A -> A -> A);
 }.
-HB.structure Definition Ring := { A of MulMonoid.axioms A & AbGroup.axioms A & Ring_of_AbGroupMulMonoid.axioms A }.
+HB.structure Definition Ring := { A of MulMonoid A & AbGroup A & Ring_of_AbGroupMulMonoid A }.
 
-HB.factory Record Ring_of_AddMulMonoid A of MulMonoid.axioms A & AddMonoid.axioms A := {
+HB.factory Record Ring_of_AddMulMonoid A of MulMonoid A & AddMonoid A := {
   opp : A -> A;
   addrC : commutative (add : A -> A -> A);
   addNr : left_inverse zero opp add;
@@ -40,7 +40,7 @@ HB.factory Record Ring_of_AddMulMonoid A of MulMonoid.axioms A & AddMonoid.axiom
   mulrDr : right_distributive mul (add : A -> A -> A);
 }.
 
-HB.builders Context A (a : Ring_of_AddMulMonoid.axioms A).
+HB.builders Context A (a : Ring_of_AddMulMonoid A).
 
   Definition to_AbGroup_of_AddMonoid :=
     AbGroup_of_AddMonoid.Axioms A opp_a addrC_a addNr_a.
@@ -54,7 +54,7 @@ HB.builders Context A (a : Ring_of_AddMulMonoid.axioms A).
 
 HB.end.
 
-HB.factory Record Ring_of_MulMonoid A of MulMonoid.axioms A := {
+HB.factory Record Ring_of_MulMonoid A of MulMonoid A := {
   zero : A;
   add : A -> A -> A;
   addrA : associative add;
@@ -67,7 +67,7 @@ HB.factory Record Ring_of_MulMonoid A of MulMonoid.axioms A := {
   mulrDr : right_distributive mul add;
 }.
 
-HB.builders Context A (a : Ring_of_MulMonoid.axioms A).
+HB.builders Context A (a : Ring_of_MulMonoid A).
 
   Definition to_AddMonoid_of_Type :=
     AddMonoid_of_Type.Axioms A zero_a add_a addrA_a add0r_a addr0_a.
diff --git a/structures.v b/structures.v
index 2342b5251..ac2b5077d 100644
--- a/structures.v
+++ b/structures.v
@@ -153,11 +153,11 @@ Elpi Export HB.status.
 
 (** [HB.mixin] declares a mixin
 
-  Syntax to create a mixin [MixinName.axioms]
-  with requirements [Factory1.axioms] .. [FactoryN.axioms]:
+  Syntax to create a mixin [MixinName]
+  with requirements [Factory1] .. [FactoryN]:
 
   <<
-  HB.mixin Record MixinName T of Factory1.axioms T & … & FactoryN.axioms T := {
+  HB.mixin Record MixinName T of Factory1 T & … & FactoryN T := {
      op : T -> …
      …
      property : forall x : T, op …
@@ -166,7 +166,7 @@ Elpi Export HB.status.
   >>
 
   Synthesizes:
-  - [MixinName.axioms T] abbreviation for the type of the (degenerate) factory
+  - [MixinName T] abbreviation for the type of the (degenerate) factory
   - [MixinName.Axioms T] abbreviation for the constructor of the factory
 
   Note: [T of f1 T & … & fN T] is ssreflect syntax for [T (_ : f1 T) … (_ : fN T)]
@@ -196,8 +196,8 @@ Elpi Export HB.mixin.
   The second syntax has a trailing [&] to pull in factory requirements silently.
 
   <<
-  HB.structure Definition StructureName := { A of Factory1.axioms A & … & FactoryN.axioms A }.
-  HB.structure Definition StructureName := { A of Factory1.axioms A & … & FactoryN.axioms A & }.
+  HB.structure Definition StructureName := { A of Factory1 A & … & FactoryN A }.
+  HB.structure Definition StructureName := { A of Factory1 A & … & FactoryN A & }.
   >>
 
 *)
@@ -245,9 +245,9 @@ Elpi Export HB.structure.
     Syntax for declaring a canonical instance:
 
     <<
-    Definition f1 : Factory1.axioms T := Factory1.Axioms T …
+    Definition f1 : Factory1 T := Factory1.Axioms T …
     …
-    Definition fN : FactoryN.axioms T := FactoryN.Axioms T …
+    Definition fN : FactoryN T := FactoryN.Axioms T …
     HB.instance T f1 … fN.
     >>
 
@@ -291,10 +291,10 @@ Elpi Export HB.factory.
 (** [HB.builders] starts a section to declare the builders associated
     to a factory. [HB.end] ends that section.
 
-    Syntax to declare builders for factory [Factory.axioms]:
+    Syntax to declare builders for factory [Factory]:
 
     <<
-    HB.builders Context A (f : Factory.axioms A).
+    HB.builders Context A (f : Factory A).
     …
     HB.instance A someFactoryInstance.
     …
@@ -304,11 +304,11 @@ Elpi Export HB.factory.
     [HB.builders] starts a section (inside a module of unspecified name) where:
     - [A] is a type variable
     - all the requirements of [Factory] were postulated as variables
-    - [f] is variable of type [Factory.axioms A]
+    - [f] is variable of type [Factory A]
     - all classes whose requirements can be obtained from [Factory] are
       declared canonical on [A]
     - for each operation [op] and property [prop] (named fields) of
-      [Factory.axioms A] a [Notation] named [op_f] and [property_f]
+      [Factory A] a [Notation] named [op_f] and [property_f]
       for the partial application of [op] and [property] to the variable [f]
 
     [HB.end] ends the section and closes the module and synthesizes
diff --git a/tests/duplicate_structure.v b/tests/duplicate_structure.v
index 8c3815dd0..75d23a2d6 100644
--- a/tests/duplicate_structure.v
+++ b/tests/duplicate_structure.v
@@ -7,5 +7,5 @@ HB.mixin Record Foo A := {
   ax : comb A op
 }.
 
-HB.structure Definition S1 := { A of Foo.axioms A }.
-Fail HB.structure Definition S2 := { A of Foo.axioms A }.
+HB.structure Definition S1 := { A of Foo A }.
+Fail HB.structure Definition S2 := { A of Foo A }.
diff --git a/tests/type_of_exported_ops.v b/tests/type_of_exported_ops.v
index 25b3be238..54924df79 100644
--- a/tests/type_of_exported_ops.v
+++ b/tests/type_of_exported_ops.v
@@ -7,7 +7,7 @@ HB.mixin Record Foo A := {
   ax : comb A op
 }.
 
-HB.structure Definition S := { A of Foo.axioms A }.
+HB.structure Definition S := { A of Foo A }.
 
 Set Printing All.
 Lemma test1 : True.

From 39e84df9c83843d0ff7cf558e866f93200d2d523 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 11 Mar 2020 11:01:52 +0100
Subject: [PATCH 3/5] Use `F.Build` rather than `F.Axioms` for the smart
 builder of F

---
 README.md           |  4 ++--
 demo1/hierarchy_1.v |  4 ++--
 demo1/hierarchy_2.v | 12 ++++++------
 demo1/hierarchy_3.v | 14 +++++++-------
 demo1/hierarchy_4.v | 18 +++++++++---------
 demo1/hierarchy_5.v | 18 +++++++++---------
 demo1/user_0.v      |  2 +-
 demo1/user_3.v      |  4 ++--
 demo2/stage10.v     | 16 ++++++++--------
 demo2/stage11.v     | 26 +++++++++++++-------------
 demo3/hierarchy_1.v |  4 ++--
 demo3/hierarchy_2.v | 10 +++++-----
 demo3/user_0.v      |  4 ++--
 hb.elpi             |  4 ++--
 readme.v            |  4 ++--
 structures.v        | 10 +++++-----
 16 files changed, 77 insertions(+), 77 deletions(-)

diff --git a/README.md b/README.md
index 535d036d0..f0b7e9796 100644
--- a/README.md
+++ b/README.md
@@ -53,9 +53,9 @@ We proceed by showing that `Z` is an example of both structures, and use
 the lemma just proved on a statement about `Z`.
 
 ```coq
-Definition Z_CoMoid := AddComoid_of_Type.Axioms Z 0%Z Z.add Z.add_assoc Z.add_comm Z.add_0_l.
+Definition Z_CoMoid := AddComoid_of_Type.Build Z 0%Z Z.add Z.add_assoc Z.add_comm Z.add_0_l.
 HB.instance Z Z_CoMoid.
-Definition Z_AbGrp := AbelianGrp_of_AddComoid.Axioms Z Z.opp Z.add_opp_diag_l.
+Definition Z_AbGrp := AbelianGrp_of_AddComoid.Build Z Z.opp Z.add_opp_diag_l.
 HB.instance Z Z_AbGrp.
 
 Lemma example2 (x : Z) : x + (- x) = - 0.
diff --git a/demo1/hierarchy_1.v b/demo1/hierarchy_1.v
index af64196bd..77a401ad7 100644
--- a/demo1/hierarchy_1.v
+++ b/demo1/hierarchy_1.v
@@ -50,11 +50,11 @@ HB.factory Record Ring_of_TYPE A := {
 HB.builders Context A (a : Ring_of_TYPE A).
 
   Definition to_AddComoid_of_TYPE :=
-    AddComoid_of_TYPE.Axioms A zero_a add_a addrA_a addrC_a add0r_a.
+    AddComoid_of_TYPE.Build A zero_a add_a addrA_a addrC_a add0r_a.
   HB.instance A to_AddComoid_of_TYPE.
 
   Definition to_Ring_of_AddComoid :=
-    Ring_of_AddComoid.Axioms A _ _ _ addNr_a mulrA_a mul1r_a
+    Ring_of_AddComoid.Build A _ _ _ addNr_a mulrA_a mul1r_a
       mulr1_a mulrDl_a mulrDr_a.
   HB.instance A to_Ring_of_AddComoid.
 
diff --git a/demo1/hierarchy_2.v b/demo1/hierarchy_2.v
index d659b0d0c..5e0fe108e 100644
--- a/demo1/hierarchy_2.v
+++ b/demo1/hierarchy_2.v
@@ -35,11 +35,11 @@ HB.factory Record AddAG_of_TYPE A := {
 HB.builders Context A (a : AddAG_of_TYPE A).
 
   Definition to_AddComoid_of_TYPE :=
-    AddComoid_of_TYPE.Axioms A zero_a add_a addrA_a addrC_a add0r_a.
+    AddComoid_of_TYPE.Build A zero_a add_a addrA_a addrC_a add0r_a.
   HB.instance A to_AddComoid_of_TYPE.
 
   Definition to_AddAG_of_AddComoid :=
-    AddAG_of_AddComoid.Axioms A _ addNr_a.
+    AddAG_of_AddComoid.Build A _ addNr_a.
   HB.instance A to_AddAG_of_AddComoid.
 
 HB.end.
@@ -68,10 +68,10 @@ HB.factory Record Ring_of_AddComoid A of AddComoid A := {
 
 HB.builders Context A (a : Ring_of_AddComoid A).
 
-  Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Axioms A _ addNr_a.
+  Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Build A _ addNr_a.
   HB.instance A to_AddAG_of_AddComoid.
 
-  Definition to_Ring_of_AddAG := Ring_of_AddAG.Axioms A
+  Definition to_Ring_of_AddAG := Ring_of_AddAG.Build A
     _ _ mulrA_a mul1r_a mulr1_a mulrDl_a mulrDr_a.
   HB.instance A to_Ring_of_AddAG.
 
@@ -98,11 +98,11 @@ HB.factory Record Ring_of_TYPE A := {
 
 HB.builders Context A (a : Ring_of_TYPE A).
 
-  Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Axioms A
+  Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Build A
     zero_a add_a addrA_a addrC_a add0r_a.
   HB.instance A to_AddComoid_of_TYPE.
 
-  Definition to_Ring_of_AddComoid := Ring_of_AddComoid.Axioms A
+  Definition to_Ring_of_AddComoid := Ring_of_AddComoid.Build A
     _ _ _ addNr_a mulrA_a mul1r_a mulr1_a mulrDl_a mulrDr_a.
   HB.instance A to_Ring_of_AddComoid.
 HB.end.
diff --git a/demo1/hierarchy_3.v b/demo1/hierarchy_3.v
index 07d11a3c6..b101ddd58 100644
--- a/demo1/hierarchy_3.v
+++ b/demo1/hierarchy_3.v
@@ -34,11 +34,11 @@ HB.factory Record AddAG_of_TYPE A := {
 
 HB.builders Context A (a : AddAG_of_TYPE A).
 
-  Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Axioms A
+  Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Build A
     zero_a add_a addrA_a addrC_a add0r_a.
   HB.instance A to_AddComoid_of_TYPE.
 
-  Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Axioms A _ addNr_a.
+  Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Build A _ addNr_a.
   HB.instance A to_AddAG_of_AddComoid.
 HB.end.
 HB.structure Definition AddAG := { A of AddAG_of_TYPE A }.
@@ -84,7 +84,7 @@ HB.builders Context A (a : Ring_of_AddAG A).
   by rewrite -mulrDr_a add0r addrC addNr.
   Qed.
 
-  Definition to_SemiRing_of_AddComoid := SemiRing_of_AddComoid.Axioms A
+  Definition to_SemiRing_of_AddComoid := SemiRing_of_AddComoid.Build A
     _ mul_a mulrA_a mulr1_a mul1r_a
     mulrDl_a mulrDr_a mul0r mulr0.
   HB.instance A to_SemiRing_of_AddComoid.
@@ -106,10 +106,10 @@ HB.factory Record Ring_of_AddComoid A of AddComoid A := {
 
 HB.builders Context A (a : Ring_of_AddComoid A).
 
-  Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Axioms A _ addNr_a.
+  Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Build A _ addNr_a.
   HB.instance A to_AddAG_of_AddComoid.
 
-  Definition to_Ring_of_AddAG := Ring_of_AddAG.Axioms A
+  Definition to_Ring_of_AddAG := Ring_of_AddAG.Build A
     _ _ mulrA_a mul1r_a mulr1_a mulrDl_a mulrDr_a.
   HB.instance A to_Ring_of_AddAG.
 
@@ -136,11 +136,11 @@ HB.factory Record Ring_of_TYPE A := {
 
 HB.builders Context A (a : Ring_of_TYPE A).
 
-  Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Axioms A
+  Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Build A
     zero_a add_a addrA_a addrC_a add0r_a.
   HB.instance A to_AddComoid_of_TYPE.
 
-  Definition to_Ring_of_AddComoid := Ring_of_AddComoid.Axioms A
+  Definition to_Ring_of_AddComoid := Ring_of_AddComoid.Build A
     _ _ _ addNr_a mulrA_a mul1r_a mulr1_a mulrDl_a mulrDr_a.
   HB.instance A to_Ring_of_AddComoid.
 HB.end.
diff --git a/demo1/hierarchy_4.v b/demo1/hierarchy_4.v
index d2dd58946..5a5032d5d 100644
--- a/demo1/hierarchy_4.v
+++ b/demo1/hierarchy_4.v
@@ -36,11 +36,11 @@ HB.builders Context A (a : AddComoid_of_TYPE A).
   Proof. by move=> x; rewrite addrC_a add0r_a. Qed.
 
   Definition to_AddMonoid_of_TYPE :=
-    AddMonoid_of_TYPE.Axioms A zero_a add_a addrA_a add0r_a addr0.
+    AddMonoid_of_TYPE.Build A zero_a add_a addrA_a add0r_a addr0.
   HB.instance A to_AddMonoid_of_TYPE.
 
   Definition to_AddComoid_of_AddMonoid :=
-    AddComoid_of_AddMonoid.Axioms A addrC_a.
+    AddComoid_of_AddMonoid.Build A addrC_a.
   HB.instance A to_AddComoid_of_AddMonoid.
 HB.end.
 HB.structure Definition AddComoid := { A of AddComoid_of_TYPE A }.
@@ -64,11 +64,11 @@ HB.factory Record AddAG_of_TYPE A := {
 HB.builders Context A (a : AddAG_of_TYPE A).
 
   Definition to_AddComoid_of_TYPE :=
-    AddComoid_of_TYPE.Axioms A zero_a add_a addrA_a addrC_a add0r_a.
+    AddComoid_of_TYPE.Build A zero_a add_a addrA_a addrC_a add0r_a.
   HB.instance A to_AddComoid_of_TYPE.
 
   Definition to_AddAG_of_AddComoid :=
-    AddAG_of_AddComoid.Axioms A _ addNr_a.
+    AddAG_of_AddComoid.Build A _ addNr_a.
   HB.instance A to_AddAG_of_AddComoid.
 HB.end.
 HB.structure Definition AddAG := { A of AddAG_of_TYPE A }.
@@ -113,7 +113,7 @@ HB.builders Context A (a : Ring_of_AddAG A).
   Qed.
 
   Definition to_SemiRing_of_AddComoid :=
-    SemiRing_of_AddComoid.Axioms A _ mul_a mulrA_a mulr1_a mul1r_a
+    SemiRing_of_AddComoid.Build A _ mul_a mulrA_a mulr1_a mul1r_a
       mulrDl_a mulrDr_a (mul0r) (mulr0).
   HB.instance A to_SemiRing_of_AddComoid.
 HB.end.
@@ -133,10 +133,10 @@ HB.factory Record Ring_of_AddComoid A of AddComoid A := {
 
 HB.builders Context A (a : Ring_of_AddComoid A).
 
-  Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Axioms A _ addNr_a.
+  Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Build A _ addNr_a.
   HB.instance A to_AddAG_of_AddComoid.
 
-  Definition to_Ring_of_AddAG := Ring_of_AddAG.Axioms A
+  Definition to_Ring_of_AddAG := Ring_of_AddAG.Build A
     _ _ mulrA_a mul1r_a mulr1_a mulrDl_a mulrDr_a.
   HB.instance A to_Ring_of_AddAG.
 
@@ -163,11 +163,11 @@ HB.factory Record Ring_of_TYPE A := {
 
 HB.builders Context A (a : Ring_of_TYPE A).
 
-  Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Axioms A
+  Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Build A
     zero_a add_a addrA_a addrC_a add0r_a.
   HB.instance A to_AddComoid_of_TYPE.
 
-  Definition to_Ring_of_AddComoid := Ring_of_AddComoid.Axioms A
+  Definition to_Ring_of_AddComoid := Ring_of_AddComoid.Build A
     _ _ _ addNr_a mulrA_a mul1r_a mulr1_a mulrDl_a mulrDr_a.
   HB.instance A to_Ring_of_AddComoid.
 HB.end.
diff --git a/demo1/hierarchy_5.v b/demo1/hierarchy_5.v
index 5b86451fd..388c6fbe6 100644
--- a/demo1/hierarchy_5.v
+++ b/demo1/hierarchy_5.v
@@ -35,11 +35,11 @@ HB.builders Context A (a : AddComoid_of_TYPE A).
   Proof. by move=> x; rewrite addrC_a add0r_a. Qed.
 
   Definition to_AddMonoid_of_TYPE :=
-    AddMonoid_of_TYPE.Axioms A zero_a add_a addrA_a add0r_a addr0.
+    AddMonoid_of_TYPE.Build A zero_a add_a addrA_a add0r_a addr0.
   HB.instance A to_AddMonoid_of_TYPE.
 
   Definition to_AddComoid_of_AddMonoid :=
-    AddComoid_of_AddMonoid.Axioms A addrC_a.
+    AddComoid_of_AddMonoid.Build A addrC_a.
   HB.instance A to_AddComoid_of_AddMonoid.
 HB.end.
 HB.structure Definition AddComoid := { A of AddComoid_of_TYPE A }.
@@ -63,11 +63,11 @@ HB.factory Record AddAG_of_TYPE A := {
 HB.builders Context A (a : AddAG_of_TYPE A).
 
   Definition to_AddComoid_of_TYPE :=
-    AddComoid_of_TYPE.Axioms A zero_a add_a addrA_a addrC_a add0r_a.
+    AddComoid_of_TYPE.Build A zero_a add_a addrA_a addrC_a add0r_a.
   HB.instance A to_AddComoid_of_TYPE.
 
   Definition to_AddAG_of_AddComoid :=
-    AddAG_of_AddComoid.Axioms A _ addNr_a.
+    AddAG_of_AddComoid.Build A _ addNr_a.
   HB.instance A to_AddAG_of_AddComoid.
 HB.end.
 HB.structure Definition AddAG := { A of AddAG_of_TYPE A }.
@@ -127,7 +127,7 @@ HB.builders Context A (a : Ring_of_AddAG A).
   by rewrite -mulrDr_a add0r addrC addNr.
   Qed.
 
-  Definition to_SemiRing_of_AddComoid := SemiRing_of_AddComoid.Axioms A
+  Definition to_SemiRing_of_AddComoid := SemiRing_of_AddComoid.Build A
     _ mul_a mulrA_a mulr1_a mul1r_a mulrDl_a mulrDr_a mul0r mulr0.
   HB.instance A to_SemiRing_of_AddComoid.
 
@@ -147,10 +147,10 @@ HB.factory Record Ring_of_AddComoid A of AddComoid A := {
 
 HB.builders Context A (a :Ring_of_AddComoid A).
 
-  Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Axioms A _ addNr_a.
+  Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Build A _ addNr_a.
   HB.instance A to_AddAG_of_AddComoid.
 
-  Definition to_Ring_of_AddAG := Ring_of_AddAG.Axioms A
+  Definition to_Ring_of_AddAG := Ring_of_AddAG.Build A
     _ _ mulrA_a mul1r_a mulr1_a mulrDl_a mulrDr_a.
   HB.instance A to_Ring_of_AddAG.
 
@@ -175,11 +175,11 @@ HB.factory Record Ring_of_TYPE A := {
 
 HB.builders Context A (a : Ring_of_TYPE A).
 
-  Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Axioms A
+  Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Build A
     zero_a add_a addrA_a addrC_a add0r_a.
   HB.instance A to_AddComoid_of_TYPE.
 
-  Definition to_Ring_of_AddComoid := Ring_of_AddComoid.Axioms A
+  Definition to_Ring_of_AddComoid := Ring_of_AddComoid.Build A
     _ _ _ addNr_a mulrA_a mul1r_a mulr1_a mulrDl_a mulrDr_a.
   HB.instance A to_Ring_of_AddComoid.
 HB.end.
diff --git a/demo1/user_0.v b/demo1/user_0.v
index 4bc06b7ad..6b0ae3e1f 100644
--- a/demo1/user_0.v
+++ b/demo1/user_0.v
@@ -3,7 +3,7 @@ From HB Require Import structures.
 From @@DEMO@@ Require Import @@HIERARCHY@@.
 
 Definition Z_ring_axioms :=
-Ring_of_TYPE.Axioms Z 0%Z 1%Z Z.add Z.opp Z.mul
+Ring_of_TYPE.Build Z 0%Z 1%Z Z.add Z.opp Z.mul
 Z.add_assoc Z.add_comm Z.add_0_l Z.add_opp_diag_l
 Z.mul_assoc Z.mul_1_l Z.mul_1_r
 Z.mul_add_distr_r Z.mul_add_distr_l.
diff --git a/demo1/user_3.v b/demo1/user_3.v
index 214c5330c..d9f823058 100644
--- a/demo1/user_3.v
+++ b/demo1/user_3.v
@@ -2,13 +2,13 @@ From Coq Require Import ZArith ssreflect.
 From HB Require Import structures.
 From @@DEMO@@ Require Import @@HIERARCHY@@.
 
-Definition Z_AddComoid := AddComoid_of_TYPE.Axioms
+Definition Z_AddComoid := AddComoid_of_TYPE.Build
   Z 0%Z Z.add
   Z.add_assoc Z.add_comm Z.add_0_l.
 
 HB.instance Z Z_AddComoid.
 
-Definition Z_SemiRing := SemiRing_of_AddComoid.Axioms
+Definition Z_SemiRing := SemiRing_of_AddComoid.Build
   Z 1%Z Z.mul
   Z.mul_assoc Z.mul_1_l Z.mul_1_r
   Z.mul_add_distr_r Z.mul_add_distr_l
diff --git a/demo2/stage10.v b/demo2/stage10.v
index 617302c9e..880fca999 100644
--- a/demo2/stage10.v
+++ b/demo2/stage10.v
@@ -106,11 +106,11 @@ HB.factory Record Ring_of_TYPE A := {
 
 HB.builders Context A (a : Ring_of_TYPE A).
 
-Definition to_AddAG_of_TYPE := AddAG_of_TYPE.Axioms A
+Definition to_AddAG_of_TYPE := AddAG_of_TYPE.Build A
     _ _ _ addrA_a addrC_a add0r_a addNr_a.
   HB.instance A to_AddAG_of_TYPE.
   Definition to_Ring_of_AddAG :=
-    Ring_of_AddAG.Axioms _ _ _ mulrA_a mul1r_a
+    Ring_of_AddAG.Build _ _ _ mulrA_a mul1r_a
       mulr1_a mulrDl_a mulrDr_a.
   HB.instance A to_Ring_of_AddAG.
 HB.end.
@@ -156,7 +156,7 @@ HB.builders Context T (a : TopologicalBase T).
   Proof. Admitted.
 
   Definition to_Topological :=
-    Topological.Axioms T _ open_of_setT (@open_of_bigcup) open_of_cap.
+    Topological.Build T _ open_of_setT (@open_of_bigcup) open_of_cap.
   HB.instance T to_Topological.
 
 HB.end.
@@ -189,7 +189,7 @@ Section ProductTopology.
   Qed.
 
   Definition prod_topology :=
-    TopologicalBase.Axioms (TopologicalSpace.sort T1 * TopologicalSpace.sort T2)%type _ prod_open_base_covers prod_open_base_setU.
+    TopologicalBase.Build (TopologicalSpace.sort T1 * TopologicalSpace.sort T2)%type _ prod_open_base_covers prod_open_base_setU.
   HB.instance ((TopologicalSpace.sort T1 * TopologicalSpace.sort T2)%type) prod_topology.
 
 End ProductTopology.
@@ -210,7 +210,7 @@ HB.structure Definition TAddAG := { A of Topological A & AddAG_of_TYPE A & JoinT
 (* Instance *)
 
 Definition Z_ring_axioms :=
-  Ring_of_TYPE.Axioms Z 0%Z 1%Z Z.add Z.opp Z.mul
+  Ring_of_TYPE.Build Z 0%Z 1%Z Z.add Z.opp Z.mul
     Z.add_assoc Z.add_comm Z.add_0_l Z.add_opp_diag_l
     Z.mul_assoc Z.mul_1_l Z.mul_1_r
     Z.mul_add_distr_r Z.mul_add_distr_l.
@@ -226,7 +226,7 @@ Lemma Qcplus_opp_l q : - q + q = 0.
 Proof. by rewrite Qcplus_comm Qcplus_opp_r. Qed.
 
 Definition Qc_ring_axioms :=
-  Ring_of_TYPE.Axioms Qc 0%Qc 1%Qc Qcplus Qcopp Qcmult
+  Ring_of_TYPE.Build Qc 0%Qc 1%Qc Qcplus Qcopp Qcmult
     Qcplus_assoc Qcplus_comm Qcplus_0_l Qcplus_opp_l
     Qcmult_assoc Qcmult_1_l Qcmult_1_r
     Qcmult_plus_distr_l Qcmult_plus_distr_r.
@@ -235,7 +235,7 @@ HB.instance Qc Qc_ring_axioms.
 Obligation Tactic := idtac.
 Definition Qcopen_base : set (set Qc) :=
   [set A | exists a b : Qc, forall z, A z <-> a < z /\ z < b].
-Program Definition QcTopological := TopologicalBase.Axioms Qc Qcopen_base _ _.
+Program Definition QcTopological := TopologicalBase.Build Qc Qcopen_base _ _.
 Next Obligation.
 move=> x _; exists [set y | x - 1 < y < x + 1].
   by exists (x - 1), (x + 1).
@@ -248,7 +248,7 @@ move=> X Y [aX [bX Xeq]] [aY [bY Yeq]] z [/Xeq [aXz zbX] /Yeq [aYz zbY]].
 Admitted.
 HB.instance Qc QcTopological.
 
-Program Definition QcJoinTAddAG := JoinTAddAG.Axioms Qc _ _.
+Program Definition QcJoinTAddAG := JoinTAddAG.Build Qc _ _.
 Next Obligation. Admitted.
 Next Obligation. Admitted.
 HB.instance Qc QcJoinTAddAG.
diff --git a/demo2/stage11.v b/demo2/stage11.v
index fef321af6..5b99e2838 100644
--- a/demo2/stage11.v
+++ b/demo2/stage11.v
@@ -110,11 +110,11 @@ HB.factory Record Ring_of_TYPE A := {
 
 HB.builders Context A (a : Ring_of_TYPE A).
 
-  Definition to_AddAG := AddAG_of_TYPE.Axioms A
+  Definition to_AddAG := AddAG_of_TYPE.Build A
     _ _ _ addrA_a addrC_a add0r_a addNr_a.
   HB.instance A to_AddAG.
 
-  Definition to_Ring := Ring_of_AddAG.Axioms A
+  Definition to_Ring := Ring_of_AddAG.Build A
     _ _ mulrA_a mul1r_a mulr1_a mulrDl_a mulrDr_a.
   HB.instance A to_Ring.
 HB.end.
@@ -161,7 +161,7 @@ HB.builders Context T (a : TopologicalBase T).
   Proof. Admitted.
 
   Definition to_Topological :=
-    Topological.Axioms T _ open_of_setT (@open_of_bigcup) open_of_cap.
+    Topological.Build T _ open_of_setT (@open_of_bigcup) open_of_cap.
   HB.instance T to_Topological.
 
 HB.end.
@@ -194,7 +194,7 @@ Section ProductTopology.
   Qed.
 
   Definition prod_topology :=
-    TopologicalBase.Axioms _ _ prod_open_base_covers prod_open_base_setU.
+    TopologicalBase.Build _ _ prod_open_base_covers prod_open_base_setU.
 
   (* TODO: make elpi insert coercions! *)
   HB.instance ((TopologicalSpace.sort T1 * TopologicalSpace.sort T2)%type) prod_topology.
@@ -242,7 +242,7 @@ Section Uniform_Topology.
   Admitted.
 
   Definition uniform_topology :=
-    Topological.Axioms _ _ uniform_open_setT (@uniform_open_bigcup) uniform_open_setI.
+    Topological.Build _ _ uniform_open_setT (@uniform_open_bigcup) uniform_open_setI.
   HB.instance (uniform (UniformSpace_wo_Topology.sort U)) uniform_topology.
 
 End Uniform_Topology.
@@ -282,7 +282,7 @@ Section TAddAGUniform.
   Admitted.
 
   Definition TAddAG_uniform :=
-    Uniform_wo_Topology.Axioms _ _ filter_TAddAG_entourage TAddAG_entourage_sub
+    Uniform_wo_Topology.Build _ _ filter_TAddAG_entourage TAddAG_entourage_sub
       TAddAG_entourage_sym TAddAG_entourage_split.
   HB.instance (TAddAG (TAddAG_wo_Uniform.sort T)) TAddAG_uniform.
 
@@ -290,7 +290,7 @@ Section TAddAGUniform.
      open = (uniform_open _ : set (set (uniform TT))).
   Admitted.
   Definition TAddAG_Join_Uniform_Topology : Join_Uniform_Topology (TAddAG T)
-    := Join_Uniform_Topology.Axioms _ TAddAG_uniform_topologyE.
+    := Join_Uniform_Topology.Build _ TAddAG_uniform_topologyE.
   HB.instance (TAddAG (TAddAG_wo_Uniform.sort T))
     TAddAG_Join_Uniform_Topology.
 
@@ -318,7 +318,7 @@ HB.builders Context U of TAddAG_Uniform U.
     (TAddAG_Join_Uniform_Topology _).
   HB.instance U to_Join_Uniform_Topology.
   Definition to_Join_TAddAG_Uniform :=
-    (Join_TAddAG_Uniform.Axioms U (TAddAG_entourageE _)).
+    (Join_TAddAG_Uniform.Build U (TAddAG_entourageE _)).
   HB.instance U to_Join_TAddAG_Uniform.
 HB.end.
 
@@ -333,14 +333,14 @@ HB.builders Context T (a : JoinTAddAG T).
   Definition to_JoinTAddAG_wo_Uniform : JoinTAddAG_wo_Uniform T := a.
   HB.instance T to_JoinTAddAG_wo_Uniform.
   (* TODO: Nice error message when factory builders do not depend on the source factory 'a'*)
-  Definition to_Uniform := let _ := a in TAddAG_Uniform.Axioms T.
+  Definition to_Uniform := let _ := a in TAddAG_Uniform.Build T.
   HB.instance T to_Uniform.
 HB.end.
 
 (* Instance *)
 
 Definition Z_ring_axioms :=
-  Ring_of_TYPE.Axioms _ 0%Z 1%Z Z.add Z.opp Z.mul
+  Ring_of_TYPE.Build _ 0%Z 1%Z Z.add Z.opp Z.mul
     Z.add_assoc Z.add_comm Z.add_0_l Z.add_opp_diag_l
     Z.mul_assoc Z.mul_1_l Z.mul_1_r
     Z.mul_add_distr_r Z.mul_add_distr_l.
@@ -354,7 +354,7 @@ Lemma Qcplus_opp_l q : - q + q = 0.
 Proof. by rewrite Qcplus_comm Qcplus_opp_r. Qed.
 
 Definition Qc_ring_axioms :=
-  Ring_of_TYPE.Axioms _ 0%Qc 1%Qc Qcplus Qcopp Qcmult
+  Ring_of_TYPE.Build _ 0%Qc 1%Qc Qcplus Qcopp Qcmult
     Qcplus_assoc Qcplus_comm Qcplus_0_l Qcplus_opp_l
     Qcmult_assoc Qcmult_1_l Qcmult_1_r
     Qcmult_plus_distr_l Qcmult_plus_distr_r.
@@ -363,7 +363,7 @@ HB.instance Qc Qc_ring_axioms.
 Obligation Tactic := idtac.
 Definition Qcopen_base : set (set Qc) :=
   [set A | exists a b : Qc, forall z, A z <-> a < z /\ z < b].
-Program Definition QcTopological := TopologicalBase.Axioms Qc Qcopen_base _ _.
+Program Definition QcTopological := TopologicalBase.Build Qc Qcopen_base _ _.
   Next Obligation.
   move=> x _; exists [set y | x - 1 < y < x + 1].
     by exists (x - 1), (x + 1).
@@ -376,7 +376,7 @@ Program Definition QcTopological := TopologicalBase.Axioms Qc Qcopen_base _ _.
   Admitted.
 HB.instance Qc QcTopological.
 
-Program Definition QcJoinTAddAG := JoinTAddAG.Axioms Qc _ _.
+Program Definition QcJoinTAddAG := JoinTAddAG.Build Qc _ _.
   Next Obligation. Admitted.
   Next Obligation. Admitted.
 HB.instance Qc QcJoinTAddAG.
diff --git a/demo3/hierarchy_1.v b/demo3/hierarchy_1.v
index fc31b38b8..33b8ceb40 100644
--- a/demo3/hierarchy_1.v
+++ b/demo3/hierarchy_1.v
@@ -44,12 +44,12 @@ HB.factory Record Ring_of_MulMonoid A of MulMonoid A := {
 HB.builders Context A (a : Ring_of_MulMonoid A).
 
   Definition to_AddMonoid_of_Type :=
-    AddMonoid_of_Type.Axioms A zero_a add_a addrA_a add0r_a addr0_a.
+    AddMonoid_of_Type.Build A zero_a add_a addrA_a add0r_a addr0_a.
 
   HB.instance A to_AddMonoid_of_Type.
 
   Definition to_Ring_of_AddMulMonoid :=
-    Ring_of_AddMulMonoid.Axioms A opp_a addrC_a addNr_a mulrDl_a mulrDr_a.
+    Ring_of_AddMulMonoid.Build A opp_a addrC_a addNr_a mulrDl_a mulrDr_a.
 
   HB.instance A to_Ring_of_AddMulMonoid.
 
diff --git a/demo3/hierarchy_2.v b/demo3/hierarchy_2.v
index b78951fc5..5eade7a23 100644
--- a/demo3/hierarchy_2.v
+++ b/demo3/hierarchy_2.v
@@ -43,12 +43,12 @@ HB.factory Record Ring_of_AddMulMonoid A of MulMonoid A & AddMonoid A := {
 HB.builders Context A (a : Ring_of_AddMulMonoid A).
 
   Definition to_AbGroup_of_AddMonoid :=
-    AbGroup_of_AddMonoid.Axioms A opp_a addrC_a addNr_a.
+    AbGroup_of_AddMonoid.Build A opp_a addrC_a addNr_a.
 
   HB.instance A to_AbGroup_of_AddMonoid.
 
   Definition to_Ring_of_AbGroupMulMonoid :=
-  Ring_of_AbGroupMulMonoid.Axioms A mulrDl_a mulrDr_a.
+  Ring_of_AbGroupMulMonoid.Build A mulrDl_a mulrDr_a.
 
   HB.instance A to_Ring_of_AbGroupMulMonoid.
 
@@ -70,17 +70,17 @@ HB.factory Record Ring_of_MulMonoid A of MulMonoid A := {
 HB.builders Context A (a : Ring_of_MulMonoid A).
 
   Definition to_AddMonoid_of_Type :=
-    AddMonoid_of_Type.Axioms A zero_a add_a addrA_a add0r_a addr0_a.
+    AddMonoid_of_Type.Build A zero_a add_a addrA_a add0r_a addr0_a.
 
   HB.instance A to_AddMonoid_of_Type.
 
   Definition to_AbGroup_of_AddMonoid :=
-    AbGroup_of_AddMonoid.Axioms A opp_a addrC_a addNr_a.
+    AbGroup_of_AddMonoid.Build A opp_a addrC_a addNr_a.
 
   HB.instance A to_AbGroup_of_AddMonoid.
 
   Definition to_Ring_of_AddMulMonoid :=
-    Ring_of_AddMulMonoid.Axioms A opp_a addrC_a addNr_a mulrDl_a mulrDr_a.
+    Ring_of_AddMulMonoid.Build A opp_a addrC_a addNr_a mulrDl_a mulrDr_a.
 
   HB.instance A to_Ring_of_AddMulMonoid.
 
diff --git a/demo3/user_0.v b/demo3/user_0.v
index 013b8b9f0..dfc241973 100644
--- a/demo3/user_0.v
+++ b/demo3/user_0.v
@@ -37,12 +37,12 @@ End Theory.
 (* Instance *)
 
 Definition Z_mulmonoid_axioms :=
-  MulMonoid_of_Type.Axioms Z 1%Z Z.mul Z.mul_assoc Z.mul_1_l Z.mul_1_r.
+  MulMonoid_of_Type.Build Z 1%Z Z.mul Z.mul_assoc Z.mul_1_l Z.mul_1_r.
 
 HB.instance Z Z_mulmonoid_axioms.
 
 Definition Z_ring_axioms :=
-  Ring_of_MulMonoid.Axioms Z 0%Z Z.add
+  Ring_of_MulMonoid.Build Z 0%Z Z.add
     Z.add_assoc Z.add_0_l Z.add_0_r
     Z.opp Z.add_comm Z.add_opp_diag_l
     Z.mul_add_distr_r Z.mul_add_distr_l.
diff --git a/hb.elpi b/hb.elpi
index a6173747b..1df08eedf 100644
--- a/hb.elpi
+++ b/hb.elpi
@@ -1237,7 +1237,7 @@ declare-factory-alias Ty1 GRFS Module TheType :- std.do! [
 
   mk-phant-mixins (global GRK) PhGRK0,
   if (mixin-first-class F _) (PhGRK = PhGRK0) (append-phant-unify PhGRK0 PhGRK),
-  mk-phant-abbrev "Axioms" PhGRK _ _,
+  mk-phant-abbrev "Build" PhGRK _ _,
 
   std.map Hyps mixin-src_mixin ML,
   main-factory-requires "axioms" (const C) ML Props SN,
@@ -1283,7 +1283,7 @@ declare-mixin-or-factory Sort1 Fields0 GRFS Module TheType D :- std.do! [
   if-verbose (coq.say "HB: declare notation Axioms"),
 
   if (D = asset-mixin) (PhGRK = PhGRK0) (append-phant-unify PhGRK0 PhGRK),
-  mk-phant-abbrev "Axioms" PhGRK _ _,
+  mk-phant-abbrev "Build" PhGRK _ _,
 
   std.map Hyps mixin-src_mixin ML,
   if (D = asset-mixin)
diff --git a/readme.v b/readme.v
index bbf3e06ff..fb00b0de7 100644
--- a/readme.v
+++ b/readme.v
@@ -30,9 +30,9 @@ Notation "- x" := (opp x).
 Lemma example (G : AbelianGrp.type) (x : G) : x + (- x) = - 0.
 Proof. by rewrite addrC addNr -[LHS](addNr zero) addrC add0r. Qed.
 
-Definition Z_CoMoid := AddComoid_of_Type.Axioms Z 0%Z Z.add Z.add_assoc Z.add_comm Z.add_0_l.
+Definition Z_CoMoid := AddComoid_of_Type.Build Z 0%Z Z.add Z.add_assoc Z.add_comm Z.add_0_l.
 HB.instance Z Z_CoMoid.
-Definition Z_AbGrp := AbelianGrp_of_AddComoid.Axioms Z Z.opp Z.add_opp_diag_l.
+Definition Z_AbGrp := AbelianGrp_of_AddComoid.Build Z Z.opp Z.add_opp_diag_l.
 HB.instance Z Z_AbGrp.
 
 Lemma example2 (x : Z) : x + (- x) = - 0.
diff --git a/structures.v b/structures.v
index ac2b5077d..4f8a0a419 100644
--- a/structures.v
+++ b/structures.v
@@ -167,7 +167,7 @@ Elpi Export HB.status.
 
   Synthesizes:
   - [MixinName T] abbreviation for the type of the (degenerate) factory
-  - [MixinName.Axioms T] abbreviation for the constructor of the factory
+  - [MixinName.Build T] abbreviation for the constructor of the factory
 
   Note: [T of f1 T & … & fN T] is ssreflect syntax for [T (_ : f1 T) … (_ : fN T)]
 *)
@@ -245,9 +245,9 @@ Elpi Export HB.structure.
     Syntax for declaring a canonical instance:
 
     <<
-    Definition f1 : Factory1 T := Factory1.Axioms T …
+    Definition f1 : Factory1 T := Factory1.Build T …
     …
-    Definition fN : FactoryN T := FactoryN.Axioms T …
+    Definition fN : FactoryN T := FactoryN.Build T …
     HB.instance T f1 … fN.
     >>
 
@@ -354,11 +354,11 @@ Elpi Export HB.end.
   Effect:
 
     Variable m0 : m0.
-    Definition s0 := S0.Pack T (S0.Axioms T m0).
+    Definition s0 := S0.Pack T (S0.Build T m0).
     Canonical s0.
     ..
     Variable mn : mn dn.
-    Definition sm : SM.Pack T (SM.Axioms T m0 .. mn).
+    Definition sm : SM.Pack T (SM.Build T m0 .. mn).
     Canonical sm.
 
   where:

From 77b137b60c531b7a59b9bf63cd5328466fbcfa43 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 11 Mar 2020 11:07:15 +0100
Subject: [PATCH 4/5] tentative fix for stage11

---
 demo2/stage11.v | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/demo2/stage11.v b/demo2/stage11.v
index 5b99e2838..32af5d80c 100644
--- a/demo2/stage11.v
+++ b/demo2/stage11.v
@@ -264,11 +264,11 @@ HB.structure Definition UniformSpace := { A of
    & Uniform_wo_Topology A }. (* TODO: should be ommited                 *)
 
 (* TODO: this is another typealias *)
-Definition TAddAG (T : Type) := T.
+Definition TAddAG_ (T : Type) := T.
 
 Section TAddAGUniform.
   Variable T : TAddAG_wo_Uniform.type.
-  Notation TT := (TAddAG T).
+  Notation TT := (TAddAG_ T).
   Definition TAddAG_entourage : set (set (TT * TT)).
   Admitted.
   Lemma filter_TAddAG_entourage : is_filter TAddAG_entourage.
@@ -284,18 +284,18 @@ Section TAddAGUniform.
   Definition TAddAG_uniform :=
     Uniform_wo_Topology.Build _ _ filter_TAddAG_entourage TAddAG_entourage_sub
       TAddAG_entourage_sym TAddAG_entourage_split.
-  HB.instance (TAddAG (TAddAG_wo_Uniform.sort T)) TAddAG_uniform.
+  HB.instance (TAddAG_ (TAddAG_wo_Uniform.sort T)) TAddAG_uniform.
 
   Lemma TAddAG_uniform_topologyE :
      open = (uniform_open _ : set (set (uniform TT))).
   Admitted.
-  Definition TAddAG_Join_Uniform_Topology : Join_Uniform_Topology (TAddAG T)
+  Definition TAddAG_Join_Uniform_Topology : Join_Uniform_Topology TT
     := Join_Uniform_Topology.Build _ TAddAG_uniform_topologyE.
-  HB.instance (TAddAG (TAddAG_wo_Uniform.sort T))
+  HB.instance (TAddAG_ (TAddAG_wo_Uniform.sort T))
     TAddAG_Join_Uniform_Topology.
 
   Lemma TAddAG_entourageE :
-    entourage = (TAddAG_entourage : set (set (TAddAG T * TAddAG T))).
+    entourage = (TAddAG_entourage : set (set (TT * TT))).
   Admitted.
 
 End TAddAGUniform.
@@ -305,7 +305,7 @@ HB.structure Definition Uniform_TAddAG_unjoined :=
   (* should be created automatically *)
 HB.mixin Record Join_TAddAG_Uniform T of Uniform_TAddAG_unjoined T := {
     entourageE :
-    entourage = (TAddAG_entourage _ : set (set (TAddAG T * TAddAG T)))
+    entourage = (TAddAG_entourage _ : set (set (TAddAG_ T * TAddAG_ T)))
 }.
 
   (* TODO: should be subsumed by the type alias TAddAG *)

From 52094ba9220bf82a73a08e16224fa1a01bcfa24b Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cohen@crans.org>
Date: Wed, 11 Mar 2020 12:48:54 +0100
Subject: [PATCH 5/5] TAddAG_ -> tAddAG

---
 demo2/stage11.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/demo2/stage11.v b/demo2/stage11.v
index 32af5d80c..3644ffd0e 100644
--- a/demo2/stage11.v
+++ b/demo2/stage11.v
@@ -264,11 +264,11 @@ HB.structure Definition UniformSpace := { A of
    & Uniform_wo_Topology A }. (* TODO: should be ommited                 *)
 
 (* TODO: this is another typealias *)
-Definition TAddAG_ (T : Type) := T.
+Definition tAddAG (T : Type) := T.
 
 Section TAddAGUniform.
   Variable T : TAddAG_wo_Uniform.type.
-  Notation TT := (TAddAG_ T).
+  Notation TT := (tAddAG T).
   Definition TAddAG_entourage : set (set (TT * TT)).
   Admitted.
   Lemma filter_TAddAG_entourage : is_filter TAddAG_entourage.
@@ -284,14 +284,14 @@ Section TAddAGUniform.
   Definition TAddAG_uniform :=
     Uniform_wo_Topology.Build _ _ filter_TAddAG_entourage TAddAG_entourage_sub
       TAddAG_entourage_sym TAddAG_entourage_split.
-  HB.instance (TAddAG_ (TAddAG_wo_Uniform.sort T)) TAddAG_uniform.
+  HB.instance (tAddAG (TAddAG_wo_Uniform.sort T)) TAddAG_uniform.
 
   Lemma TAddAG_uniform_topologyE :
      open = (uniform_open _ : set (set (uniform TT))).
   Admitted.
   Definition TAddAG_Join_Uniform_Topology : Join_Uniform_Topology TT
     := Join_Uniform_Topology.Build _ TAddAG_uniform_topologyE.
-  HB.instance (TAddAG_ (TAddAG_wo_Uniform.sort T))
+  HB.instance (tAddAG (TAddAG_wo_Uniform.sort T))
     TAddAG_Join_Uniform_Topology.
 
   Lemma TAddAG_entourageE :
@@ -305,7 +305,7 @@ HB.structure Definition Uniform_TAddAG_unjoined :=
   (* should be created automatically *)
 HB.mixin Record Join_TAddAG_Uniform T of Uniform_TAddAG_unjoined T := {
     entourageE :
-    entourage = (TAddAG_entourage _ : set (set (TAddAG_ T * TAddAG_ T)))
+    entourage = (TAddAG_entourage _ : set (set (tAddAG T * tAddAG T)))
 }.
 
   (* TODO: should be subsumed by the type alias TAddAG *)
@@ -383,4 +383,4 @@ HB.instance Qc QcJoinTAddAG.
 
 Check (entourage : set (set (Qc * Qc))). (* TODO fix spill-factory-param-factories *)
 
-End Stage11.
\ No newline at end of file
+End Stage11.