Anomaly with universes for reverse_coercion symbol

.github/workflows/nix-action-coq-8.15.yml

@@ -141,6 +141,7 @@ jobs:
   mathcomp-analysis:
     needs:
     - coq
+    - mathcomp-classical
     - hierarchy-builder
     runs-on: ubuntu-latest
     steps:
@@ -176,18 +177,10 @@ jobs:
       name: 'Building/fetching previous CI target: coq'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
         --argstr job "coq"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-ssreflect'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
-        --argstr job "mathcomp-ssreflect"
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: mathcomp-field'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
         --argstr job "mathcomp-field"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-finmap'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
-        --argstr job "mathcomp-finmap"
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: mathcomp-bigenough'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
@@ -196,6 +189,10 @@ jobs:
       name: 'Building/fetching previous CI target: mathcomp-real-closed'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
         --argstr job "mathcomp-real-closed"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-classical'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
+        --argstr job "mathcomp-classical"
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: hierarchy-builder'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
@@ -204,6 +201,64 @@ jobs:
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
         --argstr job "mathcomp-analysis"
+  mathcomp-classical:
+    needs:
+    - coq
+    - hierarchy-builder
+    runs-on: ubuntu-latest
+    steps:
+    - name: Determine which commit to test
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
+        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
+        \ | cut -f1)\n  if [ -z \"$merge_commit\" ]; then\n    echo \"tested_commit=${{\
+        \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n  else\n    echo\
+        \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n  fi\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v2
+      with:
+        fetch-depth: 0
+        ref: ${{ env.tested_commit }}
+    - name: Cachix install
+      uses: cachix/install-nix-action@v16
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup math-comp
+      uses: cachix/cachix-action@v10
+      with:
+        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
+        extraPullNames: coq, coq-community
+        name: math-comp
+    - id: stepCheck
+      name: Checking presence of CI target mathcomp-classical
+      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
+        \ bundle \"coq-8.15\" --argstr job \"mathcomp-classical\" \\\n   --dry-run\
+        \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\
+        \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: coq'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
+        --argstr job "coq"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-ssreflect'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
+        --argstr job "mathcomp-ssreflect"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-algebra'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
+        --argstr job "mathcomp-algebra"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-finmap'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
+        --argstr job "mathcomp-finmap"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: hierarchy-builder'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
+        --argstr job "hierarchy-builder"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: Building/fetching current CI target
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
+        --argstr job "mathcomp-classical"
   mathcomp-single:
     needs:
     - coq

.github/workflows/nix-action-coq-8.16.yml

@@ -35,9 +35,10 @@ jobs:
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
         --argstr job "coq"
-  coq-elpi:
+  graph-theory:
     needs:
     - coq
+    - hierarchy-builder
     runs-on: ubuntu-latest
     steps:
     - name: Determine which commit to test
@@ -63,23 +64,34 @@ jobs:
         extraPullNames: coq, coq-community
         name: math-comp
     - id: stepCheck
-      name: Checking presence of CI target coq-elpi
+      name: Checking presence of CI target graph-theory
       run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
-        \ bundle \"coq-8.16\" --argstr job \"coq-elpi\" \\\n   --dry-run 2>&1 > /dev/null)\n\
-        echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
-        \ \"built:\" | sed \"s/.*/built/\")\n"
+        \ bundle \"coq-8.16\" --argstr job \"graph-theory\" \\\n   --dry-run 2>&1\
+        \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\
+        \ | grep \"built:\" | sed \"s/.*/built/\")\n"
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: coq'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
         --argstr job "coq"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-algebra'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
+        --argstr job "mathcomp-algebra"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-fingroup'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
+        --argstr job "mathcomp-fingroup"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: hierarchy-builder'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
+        --argstr job "hierarchy-builder"
     - if: steps.stepCheck.outputs.status == 'built'
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
-        --argstr job "coq-elpi"
+        --argstr job "graph-theory"
   hierarchy-builder:
     needs:
     - coq
-    - coq-elpi
     runs-on: ubuntu-latest
     steps:
     - name: Determine which commit to test
@@ -122,10 +134,9 @@ jobs:
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
         --argstr job "hierarchy-builder"
-  mathcomp-analysis:
+  mathcomp:
     needs:
     - coq
-    - hierarchy-builder
     runs-on: ubuntu-latest
     steps:
     - name: Determine which commit to test
@@ -151,11 +162,11 @@ jobs:
         extraPullNames: coq, coq-community
         name: math-comp
     - id: stepCheck
-      name: Checking presence of CI target mathcomp-analysis
+      name: Checking presence of CI target mathcomp
       run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
-        \ bundle \"coq-8.16\" --argstr job \"mathcomp-analysis\" \\\n   --dry-run\
-        \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\
-        \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n"
+        \ bundle \"coq-8.16\" --argstr job \"mathcomp\" \\\n   --dry-run 2>&1 > /dev/null)\n\
+        echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
+        \ \"built:\" | sed \"s/.*/built/\")\n"
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: coq'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
@@ -165,29 +176,32 @@ jobs:
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
         --argstr job "mathcomp-ssreflect"
     - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-field'
+      name: 'Building/fetching previous CI target: mathcomp-fingroup'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
-        --argstr job "mathcomp-field"
+        --argstr job "mathcomp-fingroup"
     - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-finmap'
+      name: 'Building/fetching previous CI target: mathcomp-algebra'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
-        --argstr job "mathcomp-finmap"
+        --argstr job "mathcomp-algebra"
     - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-real-closed'
+      name: 'Building/fetching previous CI target: mathcomp-solvable'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
-        --argstr job "mathcomp-real-closed"
+        --argstr job "mathcomp-solvable"
     - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: hierarchy-builder'
+      name: 'Building/fetching previous CI target: mathcomp-field'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
-        --argstr job "hierarchy-builder"
+        --argstr job "mathcomp-field"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-character'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
+        --argstr job "mathcomp-character"
     - if: steps.stepCheck.outputs.status == 'built'
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
-        --argstr job "mathcomp-analysis"
+        --argstr job "mathcomp"
   mathcomp-single:
     needs:
     - coq
-    - coq-elpi
     - hierarchy-builder
     runs-on: ubuntu-latest
     steps:
@@ -238,7 +252,6 @@ jobs:
   mathcomp-single-planB-src:
     needs:
     - coq
-    - coq-elpi
     - hierarchy-builder
     runs-on: ubuntu-latest
     steps:

.nix/config.nix

@@ -1,7 +1,7 @@
 {
   format = "1.0.0";
   attribute = "hierarchy-builder";
-  default-bundle = "coq-8.15";
+  default-bundle = "coq-rev_coerce";
   bundles = let
     mcHBcommon = {
       mathcomp.override.version = "hierarchy-builder";
@@ -33,6 +33,10 @@
     "coq-8.15".coqPackages = {
       coq.override.version = "8.15";
     };
+    "coq-rev_coerce".coqPackages = {
+      coq.override.version = "proux01:rev_coerce";
+      coq-elpi.override.version = "coq-master";
+    };
   };
   cachix.coq = {};
   cachix.coq-community = {};

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"be976db262f1dc9f6e013153f263182e14372246"
+"4f0eb194b37b6e0db28be2eb4643bd6924abf7ab"

Changelog.md

@@ -1,5 +1,32 @@
 # Changelog
 
+## UNRELEASED
+
+## [1.4.0] - 2022-09-29
+
+Compatible with
+- Coq 8.15 with Coq-Elpi 1.14.x
+- Coq 8.16 with Coq-Elpi 1.15.x and 1.16.x
+
+### General
+
+- **Fix** `HB.pack` works with structures about functions, and not just types.
+- **Fix** `HB.about` and `HB.graph` now display shortest names.
+- **New** Command `HB.howto` to find all possible ways to instanciate structures.
+- **New** Structures now support keys which type's head is a global reference.
+  (Only keys corresponding to the coercion classes `Sortclass` and `Funclass` were accepted).
+
+## [1.3.0] - 2022-07-27
+
+Compatible with
+- Coq 8.15 with Coq-Elpi 1.14.x
+- Coq 8.16 with Coq-Elpi 1.15.x
+
+### General
+
+- **Fix** Structures can be keyd on sorts (eg `Prop`) and products (eg `T -> U`)
+- **New** Mixin parameters can depend on structure instances inferred using previous mixins (see [this test](tests/interleave_context.v))
+
 ## [1.2.1] - 2022-01-10
 
 Compatible with

HB/about.elpi

@@ -15,7 +15,7 @@ main-located S (loc-gref GR) :- class-def (class Class GR MLwP), !,
   private.main-structure S Class GR MLwP.
 
 main-located _ (loc-gref Class) :- class-def (class Class GR MLwP), !,
-  gref->modname GR 2 "." M,
+  gref->modname_short GR "." M,
   coq.gref->id GR St,
   S is M ^ "." ^ St,
   private.main-structure S Class GR MLwP.
@@ -45,7 +45,7 @@ main-located S (loc-gref GR) :- from Factory Mixin GR, !,
   private.main-builder S Factory Mixin.
 
 main-located S (loc-gref GR) :-
-  std.filter {coq.CS.db-for _ (cs-gref GR)} (private.not1 private.unif-hint?) LV,
+  std.filter {coq.CS.db-for _ (cs-gref GR)} (not1 unif-hint?) LV,
   coq.CS.db-for GR _ LP,
   std.filter {coq.coercion.db} (c\c = coercion GR _ _ _) LC,
   if (LV = [], LP = [], LC = [])
@@ -57,6 +57,29 @@ main-located S (loc-gref GR) :-
 
 main-located S (loc-abbreviation _) :- coq.error "HB: unknown abbreviation" S.
 
+/* things also used in paths.elpi ------------------------------------------ */
+
+shorten coq.pp.{ v , h, hv, hov , spc , str , box , glue , brk , empty }.
+
+pred bulletize1 i:(A -> coq.pp -> prop), i:A, o:coq.pp.
+bulletize1 F X (glue [str "- ", M]) :- F X M.
+
+pred bulletize i:list A, i:(A -> coq.pp -> prop), o:coq.pp.
+bulletize [] _ empty.
+bulletize L F (glue [brk 0 0 | PLB]) :-
+  std.map L (bulletize1 F) PL,
+  std.intersperse (brk 0 0) PL PLB.
+
+% Print shortest qualified identifier of the module containing a gref
+pred pp-module i:gref, o:coq.pp.
+pp-module GR (str ID) :- gref->modname_short GR "." ID.
+
+pred unif-hint? i:cs-instance.
+unif-hint? (cs-instance _ (cs-gref GR) _) :- coq.CS.db-for GR _ [_|_].
+
+pred not1 i:(A -> prop), i:A.
+not1 P X :- not (P X).
+
 
 /* ------------------------------------------------------------------------- */
 /* ----------------------------- private code ------------------------------ */
@@ -76,7 +99,7 @@ main-canonical-value S CanonicalValues :-
   group-by-loc CanonicalValues CanonicalValuesL,
   %format
   PpCanonicalValues = box (v 4) [
-    str "HB: ", str S, str " is canonically equipped with mixins:",
+    str "HB: ", str S, str " is canonically equipped with structures:",
     {bulletize CanonicalValuesL pp-canonical-solution-list}],
   % print
   coq.say {coq.pp->string PpCanonicalValues},
@@ -101,7 +124,7 @@ pred pp-canonical-solution i:cs-instance, o:coq.pp.
 pp-canonical-solution (cs-instance _Proj _Pat GR) Pp :-
   coq.env.typeof GR T,
   coq.prod-tgt->gref T F,
-  if (class-def (class _ F _)) (gref->modname F 2 "." ID) (coq.gref->string F ID),
+  if (class-def (class _ F _)) (gref->modname_short F "." ID) (coq.gref->string F ID),
   Pp = box (hov 0) [ str ID ].
 
 pred main-canonical-projection i:string, i:gref, i:list cs-instance.
@@ -127,11 +150,11 @@ pred main-coercion i:string, i:list coercion.
 main-coercion S [coercion GR _ Src Tgt|_] :-
   % format
   if (class-def (class _ Src _) ; class-def (class Src _ _))
-     (Source = str {gref->modname Src 2 "."})
+     (Source = str {gref->modname_short Src "."})
      (coq.term->pp (global Src) Source),
   if2 (Tgt = grefclass TGR)
         (if (class-def (class _ TGR _) ; class-def (class TGR _ _))
-          (Target = str {gref->modname TGR 2 "."})
+          (Target = str {gref->modname_short TGR "."})
           (coq.term->pp (global TGR) Target))
       (Tgt = sortclass)
         (Target = str "Sortclass")
@@ -306,7 +329,7 @@ main-factory-alias S _Const :-
 pred main-builder i:string, i:factoryname, i:mixinname.
 main-builder _S From To :-
   coq.say "HB: todo HB.about for builder from"
-    {gref->modname From 2 "."} "to" {gref->modname To 2 "."}.
+    {gref->modname_short From "."} "to" {gref->modname_short To "."}.
 
 pred compute-field-info.aux i:list id, i:list implicit_kind, o:list coq.pp.
 compute-field-info.aux [] _ [].
@@ -323,9 +346,6 @@ compute-field-info Names Impls O :-
   compute-field-info.aux {std.rev Names} {std.rev Impls} Pp,
   std.intersperse spc {std.rev Pp} O.
 
-pred pp-module i:gref, o:coq.pp.
-pp-module M (str ID) :- gref->modname M 2 "." ID.
-
 pred pp-const i:constant, o:coq.pp.
 pp-const F (str ID) :- coq.gref->id (const F) ID.
 
@@ -336,15 +356,6 @@ pred pp-if-verbose o:coq.pp, i:(coq.pp -> prop).
 pp-if-verbose V P :- get-option "verbose" tt, !, P V.
 pp-if-verbose empty _.
 
-pred bulletize1 i:(A -> coq.pp -> prop), i:A, o:coq.pp.
-bulletize1 F X (glue [str "- ", M]) :- F X M.
-
-pred bulletize i:list A, i:(A -> coq.pp -> prop), o:coq.pp.
-bulletize [] _ empty.
-bulletize L F (glue [brk 0 0 | PLB]) :-
-  std.map L (bulletize1 F) PL,
-  std.intersperse (brk 0 0) PL PLB.
-
 pred pp-loc-of i:gref, o:coq.pp.
 pp-loc-of GR PP :- decl-location GR Loc, !, pp-loc Loc PP.
 pp-loc-of _ coq.pp.empty.
@@ -377,10 +388,4 @@ print-docstring GR :-
      (coq.say {coq.pp->string (box (hov 5) [str"Doc: ",Doc])})
      true.
 
-pred unif-hint? i:cs-instance.
-unif-hint? (cs-instance _ (cs-gref GR) _) :- coq.CS.db-for GR _ [_|_].
-
-pred not1 i:(A -> prop), i:A.
-not1 P X :- not (P X).
-
 }}

HB/common/log.elpi

@@ -35,6 +35,7 @@ env.add-const-noimplicits Name Bo Ty Opaque C :- std.do! [
                ":" {coq.term->string Ty} ":=" {coq.term->string Bo})
     true,
   avoid-name-collision Name Name1,
+  coq.typecheck Bo Ty _,
   coq.env.add-const Name1 Bo Ty Opaque C,
   env.add-location (const C),
   if (var Ty) (Ty? = none) (Ty? = some Ty),
@@ -49,6 +50,7 @@ env.add-const Name Bo Ty Opaque C :- std.do! [
                ":" {coq.term->string Ty} ":=" {coq.term->string Bo})
     true,
   avoid-name-collision Name Name1,
+  coq.typecheck Bo Ty _,
   coq.env.add-const Name1 Bo Ty Opaque C,
   env.add-location (const C),
   if (var Ty) (Ty? = none) (Ty? = some Ty),
@@ -61,6 +63,7 @@ env.add-const-noimplicits-failondup 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.typecheck Bo Ty _,
   coq.env.add-const Name Bo Ty Opaque C,
   env.add-location (const C),
   if (var Ty) (Ty? = none) (Ty? = some Ty),
@@ -266,8 +269,8 @@ pred log.private.log-tactic i:term.
 
 with-logging P :- (get-option "elpi.hb.log" _, NICE = tt ; get-option "elpi.hb.log.raw" _, NICE = ff), !,
   get-option "elpi.loc" Loc,
-  loc.fields Loc FILE _ _ _ _,
-  std.any->string Loc LocStr,
+  loc.fields Loc FILE Start Stop _ _,
+  LocStr is "characters " ^ {std.any->string Start} ^ "-" ^ {std.any->string Stop},
   FILENAME is FILE ^ ".hb",
   open_append FILENAME OC1,
   std.string.concat "\n" ["","HIERARCHY BUILDER PATCH v1",LocStr,""] PATCH1,
@@ -295,7 +298,7 @@ log.private.log-vernac _.
 
 log.private.log-tactic P :- log.private.logger L Nice, !,
   if (Nice = tt) (PPALL = []) (PPALL = [@ppall!]),
-  log.private.logger-extend L {PPALL => coq.term->pp P}.
+  log.private.logger-extend L {PPALL => @holes! => coq.term->pp P}.
 log.private.log-tactic _.
 
 % The main entry point to print vernacular commands is coq.vernac->pp
@@ -361,7 +364,7 @@ coq.vernac->pp1 (abbreviation Name NParams Term) (box (hv 2) [box h [str "Notati
   coq.vernac->ppabbrterm NParams Term StrParams B.
 coq.vernac->pp1 (canonical Name Local) (box h [Locality, str "Canonical ", str Name, str "."]) :-
   local->locality Local Locality.
-coq.vernac->pp1 (coercion Name SRC TGT) (box h [str "Coercion ", str Name, str " : ", str S, str " >-> ", str T, str "."]) :-
+coq.vernac->pp1 (coercion Name SRC TGT) (box h [str "#[reversible] Coercion ", str Name, str " : ", str S, str " >-> ", str T, str "."]) :-
   coq.gref->path SRC SP, std.string.concat "." {std.take-last 2 SP} S', S is S' ^ "." ^ {coq.gref->id SRC},
   if2 (TGT = sortclass) (T = "Sortclass")
       (TGT = funclass)  (T = "Funclass")
@@ -446,8 +449,8 @@ coq.vernac->ppinductiveconstructor [constructor ID Arity|Ks] PP :-
 pred coq.vernac->ppinductiveparams i:list (pair implicit_kind term), o:list coq.pp.
 coq.vernac->ppinductiveparams [] [].
 coq.vernac->ppinductiveparams [pr Imp T|Rest] PP :-
-  PP = [box (hov 2) [str A,str ID,str " : ", TY,str B]|PPRest],
-  decl T Name Ty, coq.name->id Name ID, coq.term->pp Ty TY,
+  PP = [box (hov 2) [str A,ID,str " : ", TY,str B]|PPRest],
+  coq.term->pp T ID, decl T _ Ty, coq.term->pp Ty TY,
   if2 (Imp = explicit) (A = "(", B = ")")
       (Imp = maximal)  (A = "{", B = "}")
                        (A = "[", B = "]"),

HB/common/phant-abbreviation.elpi

@@ -92,7 +92,10 @@ fun-infer-type funclass N Ty (t\private.phant-term AL (Bo t)) Out :-
   coq.name-suffix N "ph" PhN,
   fun-implicit N Ty (t\private.phant-term [private.infer-type N funclass|AL]
                                           (fun PhN {{ lib:@hb.phantom (_ -> _) lp:t }} _\ Bo t)) Out.
-fun-infer-type C _ _ _ _  :- coq.error "HB: inference of parameters of call" C "not implemented yet".
+fun-infer-type (grefclass Class) N Ty (t\private.phant-term AL (Bo t)) Out :-
+  coq.name-suffix N "ph" PhN, private.build-type-pattern Class Pat,
+  fun-implicit N Ty (t\private.phant-term [private.infer-type N (grefclass Class)|AL]
+                                          (fun PhN {{ lib:@hb.phantom lp:Pat lp:t }} _\ Bo t)) Out.
 
 % TODO: this looks like a hack to remove
 pred append-fun-unify i:phant-term, o:phant-term.
@@ -180,12 +183,25 @@ build-abbreviation K F [infer-type N sortclass|AL] K'' (fun N _ AbbrevFx) :- !,
 build-abbreviation K F [infer-type N funclass|AL] K'' (fun N _ AbbrevFx) :- !,
   pi x\ build-abbreviation K {mk-app F [{{ lib:hb.Phantom (_ -> _) lp:x }}]} AL K' (AbbrevFx x),
   K'' is K' + 1.
-build-abbreviation _ _ [infer-type _ (grefclass _)|_] _ _ :- coq.error "TODO".
+build-abbreviation K F [infer-type N (grefclass Class)|AL] K'' (fun N _ AbbrevFx) :- !,
+  build-type-pattern Class Pat,
+  pi x\ build-abbreviation K {mk-app F [{{ lib:hb.Phantom lp:Pat lp:x }}]} AL K' (AbbrevFx x),
+  K'' is K' + 1.
 build-abbreviation K F [implicit|AL] K' FAbbrev :- !,
   build-abbreviation K {mk-app F [_]} AL K' FAbbrev.
 build-abbreviation K F [unify|AL] K' FAbbrev :- !,
   build-abbreviation K {mk-app F [{{lib:@hb.id _ _}}]} AL K' FAbbrev.
 
+% [build-type-pattern GR Pat] cheks that GR : forall x_1 ... x_n, Type
+% and returns Pat = GR _ ... _ (that is GR  applied to n holes).
+% Note that n can be 0 when GR : Type.
+pred build-type-pattern i:gref, o:term.
+build-type-pattern GR Pat :- build-type-pattern.aux GR {coq.env.typeof GR} Pat.
+build-type-pattern.aux GR T {{ lp:Pat _ }} :- coq.unify-eq T (prod N S T') ok, !,
+  @pi-decl N S x\ build-type-pattern.aux GR (T' x) Pat.
+build-type-pattern.aux GR T (global GR) :- coq.unify-eq T {{ Type }} ok, !.
+build-type-pattern.aux _ _ _ :- coq.error "HB: wrong carrier type".
+
 
 % [mk-phant-term F PF] states that
 % if F = fun p1 .. p_k T m_0 .. m_n => _

HB/common/stdpp.elpi

@@ -48,6 +48,25 @@ under.do! Then LP :- Then (_\ std.do! LP) _.
 pred map-triple i:(A -> A1 -> prop), i:(B -> B1 -> prop), i:(C -> C1 -> prop), i:triple A B C, o:triple A1 B1 C1.
 map-triple F G H (triple X Y Z) (triple X1 Y1 Z1) :- F X X1, G Y Y1, H Z Z1.
 
+pred sort.split i:list A, o:list A, o:list A.
+sort.split [] [] [] :- !.
+sort.split [X] [X] [] :- !.
+sort.split [X,Y|TL] [X|L1] [Y|L2] :- sort.split TL L1 L2.
+
+pred sort.merge i:(A -> A -> prop), i:list A, i:list A, o:list A.
+sort.merge _ [] L L :- !.
+sort.merge _ L [] L :- !.
+sort.merge Rel [X1|L1] [X2|L2] [X1|M] :- Rel X1 X2, !,
+  sort.merge Rel L1 [X2|L2] M.
+sort.merge Rel [X1|L1] [X2|L2] [X2|M] :-
+  sort.merge Rel [X1|L1] L2 M.
+
+pred sort i:list A, i:(A -> A -> prop), o:list A.
+sort [] _ [] :- !.
+sort [X] _ [X] :- !.
+sort L Rel M :-
+  sort.split L L1 L2, sort L1 Rel S1, sort L2 Rel S2, sort.merge Rel S1 S2 M.
+
 pred bubblesort i:list A, i:(A -> A -> prop), o:list A.
 bubblesort [] _ [] :- !.
 bubblesort [X] _ [X] :- !.
@@ -101,8 +120,7 @@ constraint print-ctx mixin-src {
 
 % approximation, it should be logical path, not the file name
 pred coq.env.current-library o:string.
-coq.env.current-library L :- coq.version _ _ N _, N >= 13, !,
-  loc.fields {get-option "elpi.loc"} L _ _ _ _.
+coq.env.current-library L :- loc.fields {get-option "elpi.loc"} L _ _ _ _.
 coq.env.current-library "dummy.v".
 
 pred coq.prod-tgt->gref i:term, o:gref.

HB/common/synthesis.elpi

@@ -154,8 +154,7 @@ infer-coercion-tgt (w-params.cons ID Ty F) CoeClass :-
   @pi-parameter ID Ty x\ infer-coercion-tgt (F x) CoeClass.
 infer-coercion-tgt (w-params.nil _ {{ Type }} _) sortclass.
 infer-coercion-tgt (w-params.nil _ {{ _ -> _ }} _) funclass.
-infer-coercion-tgt (w-params.nil _ _ _) _ :-
-  coq.error "HB: coercion not to Sortclass or Funclass not supported yet.".
+infer-coercion-tgt (w-params.nil _ T _) (grefclass GR) :- coq.term->gref T GR.
 
 pred w-args.check-key i:list term, i:term, i:list (w-args A), o:prop.
 w-args.check-key _PS _T [] true :- !.

HB/common/utils.elpi

@@ -120,29 +120,43 @@ nice-gref->string X Mod :-
 nice-gref->string X S :-
   coq.term->string (global X) S.
 
-pred compat.concat i:string, i:list string, o:string.
-compat.concat S L O :- coq.version _ _ N _, N > 12, !, std.string.concat S L O.
-compat.concat S L O :- compat.concat.aux L S O.
-compat.concat.aux [] _ "".
-compat.concat.aux [X] _ X :- !.
-compat.concat.aux [X|XS] Sep O :- compat.concat.aux XS Sep O1, O is X ^ Sep ^ O1.
-
 pred gref->modname i:gref, i:int, i:string, o:string.
 gref->modname GR NComp Sep ModName :-
   coq.gref->path GR Path,
   std.rev Path Mods,
   std.length Path Len,
   if (Len >= NComp) true (coq.error "Not enough enclosing modules for" {coq.gref->string GR}),
   std.take NComp Mods L,
-  compat.concat Sep {std.rev L} ModName.
+  std.string.concat Sep {std.rev L} ModName.
 pred gref->modname-label i:gref, i:int, i:string, o:string.
 gref->modname-label GR NComp Sep ModName :-
   coq.gref->path GR Path,
   std.rev Path PathRev,
   std.length PathRev Len,
   if (Len >= NComp) (N = NComp) (N = Len),
   std.take N PathRev L,
-  compat.concat Sep {std.rev [{coq.gref->id GR}|L]} ModName.
+  std.string.concat Sep {std.rev [{coq.gref->id GR}|L]} ModName.
+
+pred string->modpath i:string, o:modpath.
+string->modpath S MP :-
+  std.filter {coq.locate-all S} (l\l = loc-modpath _) L,
+  L = [loc-modpath MP].
+
+pred gref->modname_short1 i:modpath, i:string, i:list string, o:string.
+gref->modname_short1 _ S [] S.
+gref->modname_short1 MP "" [X|L] L' :- gref->modname_short1 MP X L L'.
+gref->modname_short1 MP S _ S :- string->modpath S MP.
+gref->modname_short1 MP S [X|L] S' :-
+  gref->modname_short1 MP {std.string.concat "." [X,S]} L S'.
+
+% Print shortest qualified identifier of the module containing a gref
+% Sep is used as separator
+pred gref->modname_short i:gref, i:string, o:string.
+gref->modname_short GR Sep IDS :-
+  coq.gref->path GR Path,
+  string->modpath {std.string.concat "." Path} MP,
+  gref->modname_short1 MP "" {std.rev Path} ID,
+  rex.replace "[.]" Sep ID IDS.
 
 pred avoid-name-collision i:string, o:string.
 avoid-name-collision S S1 :-

HB/graph.elpi

@@ -18,27 +18,11 @@ to-file File :- !, std.do! [
 
 namespace private {
 
-pred compat.concat i:string, i:list string, o:string.
-compat.concat S L O :- coq.version _ _ N _, N > 12, !, std.string.concat S L O.
-compat.concat S L O :- compat.concat.aux L S O.
-compat.concat.aux [] _ "".
-compat.concat.aux [X] _ X :- !.
-compat.concat.aux [X|XS] Sep O :- compat.concat.aux XS Sep O1, O is X ^ Sep ^ O1.
-
-pred gref->modname i:gref, i:int, i:string, o:string.
-gref->modname GR NComp Sep ModName :-
-  coq.gref->path GR Path,
-  std.rev Path Mods,
-  std.length Path Len,
-  if (Len >= NComp) true (coq.error "Not enough enclosing modules for" {coq.gref->string GR}),
-  std.take NComp Mods L,
-  compat.concat Sep {std.rev L} ModName.
-
 pred pp-coercion-dot i:out_stream, i:coercion. 
 pp-coercion-dot OC (coercion _ _ Src (grefclass Tgt)) :- class-def (class Src _ _), class-def (class Tgt _ _), !, std.do! [
-  output OC {gref->modname Tgt 2 "_"},
+  output OC {gref->modname_short Tgt "_"},
   output OC " -> ",
-  output OC {gref->modname Src 2 "_"},
+  output OC {gref->modname_short Src "_"},
   output OC ";\n",
 ].
 pp-coercion-dot _ _.

HB/howto.elpi

@@ -0,0 +1,158 @@
+/*        Hierarchy Builder: algebraic hierarchies made easy
+    This software is released under the terms of the MIT license              */
+
+namespace howto {
+
+pred main-trm i:term, i:string, i:option int.
+main-trm T STgt Depth :- coq.term->gref T GR, main-gref GR STgt Depth.
+
+pred main-str i:string, i:string, i:option int.
+main-str S STgt Depth :- coq.locate S GR, main-gref GR STgt Depth.
+
+pred main-gref i:gref, i:string, i:option int.
+main-gref GR STgt Depth :- class-def (class _ GR _), !,
+  private.mixins-in-structures [GR] MLSrc,
+  main-from MLSrc STgt Depth.
+main-gref GR STgt Depth :-
+  private.structures-on-gref GR SL,
+  private.mixins-in-structures SL MLSrc,
+  main-from MLSrc STgt Depth.
+
+pred main-from i:list mixinname, i:string, i:option int.
+main-from MLSrc STgt Depth :-
+  private.mixins-in-structures [{coq.locate STgt}] MLTgt,
+  private.list-diff MLTgt MLSrc ML,
+  if (ML = []) (coq.say "HB: nothing to do.") (main-from.aux MLSrc ML Depth).
+main-from.aux MLSrc ML (some Depth) :- main-increase-depth MLSrc ML Depth false.
+main-from.aux MLSrc ML none :- main-increase-depth MLSrc ML 3 true.
+
+pred main-increase-depth i:list mixinname, i:list mixinname, i:int, i:prop.
+main-increase-depth MLSrc ML Depth AutoIncrease :-
+  private.paths-from-for-step MLSrc ML Depth R,
+  if (not (R = [])) (private.pp-solutions R)
+  (if AutoIncrease
+    (Depth' is Depth + 1,
+     coq.say "HB: no solution found at depth" Depth "looking at depth" Depth',
+     main-increase-depth MLSrc ML Depth' true)
+    (coq.error "HB: no solution found, try to increase search depth.")).
+
+
+/* ------------------------------------------------------------------------- */
+/* ----------------------------- private code ------------------------------ */
+/* ------------------------------------------------------------------------- */
+
+namespace private {
+
+shorten coq.pp.{ v , hov , spc , str , box , glue }.
+
+% L1 \subseteq L2
+pred incl i:list A, i:list A.
+incl L1 L2 :- std.forall L1 (std.mem L2).
+
+% R = L1 \ L2
+pred list-diff i:list A, i:list A, o:list A.
+list-diff L1 L2 R :- std.filter L1 (about.not1 (std.mem L2)) R.
+
+% R = L1 U L2
+pred union i:list A, i:list A, o:list A.
+union L1 L2 R :-
+  std.fold L2 L1 (x\l\l'\if (std.mem l x) (l' = l) (l' = [x|l])) R.
+
+pred insert-sorted i:(A -> A -> prop), i:A, i:list A, o:list A.
+insert-sorted _ X [] [X] :- !.
+insert-sorted Rel X [Y|T] [X,Y|T] :- Rel X Y, !.
+insert-sorted Rel X [Y|T] [Y|T'] :- insert-sorted Rel X T T', !.
+
+pred lt-gref i:gref, i:gref.
+lt-gref X Y :-
+  gref->modname_short X "." SX, gref->modname_short Y "." SY, !, SX s< SY.
+
+pred size-order i:(list A -> list A -> prop), i:list A, i:list A.
+size-order Rel L1 L2 :-
+  std.length L1 S1, std.length L2 S2, !, (S1 i< S2; (S1 = S2, !, Rel L1 L2)).
+
+pred lexi-order i:list gref, i:list gref.
+lexi-order [] [].
+lexi-order [X1|_] [X2|_] :- lt-gref X1 X2.
+lexi-order [X|T1] [X|T2] :- lexi-order T1 T2.
+
+% [structures-on-gref GR ML] list structures [GR] is equipped with
+pred structures-on-gref i:gref, o:list structure.
+structures-on-gref GR SL :-
+  std.filter {coq.CS.db-for _ (cs-gref GR)} (about.not1 about.unif-hint?) LV,
+  std.map LV structures-on-gref.aux SL.
+structures-on-gref.aux (cs-instance _ _ GR) F :-
+  coq.prod-tgt->gref {coq.env.typeof GR} F, class-def (class _ F _).
+
+% [mixins-in-structures SL ML] list mixins in structures [SL]
+pred mixins-in-structures i:list structure, o:list mixinname.
+mixins-in-structures SL ML :- std.fold SL [] mixins-in-structures.aux ML.
+mixins-in-structures.aux F L L' :-
+  class-def (class _ F MLWP), union L {list-w-params_list MLWP} L'.
+
+% a type to store a factory along with the mixins it depends on
+% and the mixins it provides
+kind factory_deps_prov type.
+type fdp factoryname -> list mixinname -> list mixinname -> factory_deps_prov.
+
+% get all available factories in the above type
+pred list_factories o:list factory_deps_prov.
+list_factories FL :-
+  std.map-filter {std.findall (factory-constructor _ _)} list_factories.aux FL.
+list_factories.aux (factory-constructor F _) (fdp F DML PML) :-
+  list-w-params_list {gref-deps F} DML,
+  list-w-params_list {factory-provides F} PML.
+
+% [paths-from-for-step MLSrc ML K R] returns in [R] a list of sequences
+% of at most [K] factories that could, starting from mixins [MLSrc],
+% build exactly the mixins [ML]
+pred paths-from-for-step i:list mixinname, i:list mixinname, i:int,
+    o:list (list factoryname).
+paths-from-for-step MLSrc ML K R :-
+  std.filter {list_factories} (fd\sigma pml\fd = fdp _ _ pml, incl pml ML) FL,
+  paths-from-for-step-using MLSrc ML K [] [] FL _ R.
+
+% [paths-from-for-step-using MLSrc ML K Pre KnownPre FL KnownPre' R]
+% same as [paths-from-for-step MLSrc ML K R] using only factories in [FL]
+% [Pre] is a (sorted) prefix that is looked into the list of known (sorted)
+% prefixes [KnownPre] to avoid generating identical solutions up to permutations
+pred paths-from-for-step-using i:list mixinname, i:list mixinname, i:int,
+    i:list factoryname, i:list (list factoryname), i:list factory_deps_prov,
+    o:list (list factoryname), o:list (list factoryname).
+paths-from-for-step-using _ _ K _ KnownPre _ KnownPre [] :- K i< 0.
+paths-from-for-step-using _ _ _ Pre KnownPre _ KnownPre [] :-
+  std.mem KnownPre Pre, !.
+paths-from-for-step-using _ [] _ Pre KnownPre _ [Pre|KnownPre] [[]] :- !.
+paths-from-for-step-using MLSrc ML K Pre KnownPre FL [Pre|KnownPre'] R :-
+  K' is K - 1,
+  std.filter FL (p\sigma dml\p = fdp _ dml _, incl dml MLSrc) FLdep,
+  std.fold FLdep (pr KnownPre [])
+    (paths-from-for-step-using.aux MLSrc ML FL K' Pre)
+    (pr KnownPre' R).
+paths-from-for-step-using.aux MLSrc ML FL' K' Pre (fdp F _ MLF) (pr KnPre L)
+    (pr KnPre' R) :-
+  std.append MLSrc MLF MLSrc',
+  list-diff ML MLF ML',
+  insert-sorted lt-gref F Pre Pre',
+  std.filter FL' (p\sigma pml\p = fdp _ _ pml, incl pml ML') FML',
+  paths-from-for-step-using MLSrc' ML' K' Pre' KnPre FML' KnPre' R',
+  std.map R' (l\r\r = [F|l]) R'',
+  std.append L R'' R.
+
+pred pp-solutions i:list (list factoryname).
+pp-solutions LLF :-
+  std.sort LLF (size-order lexi-order) SLLF,
+  % format
+  PpSolutions = box (v 4) [
+    str "HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):",
+    {about.bulletize SLLF pp-solution}],
+  % print
+  coq.say {coq.pp->string PpSolutions},  
+  coq.say.
+
+pred pp-solution i:list factoryname o:coq.pp.
+pp-solution L (box (hov 0) PLS) :-
+  std.map L about.pp-module PL,
+  std.intersperse (glue [str ";", spc]) PL PLS.
+
+}}

HB/instance.elpi

@@ -370,7 +370,7 @@ check-non-forgetful-inheritance T Factory :- std.do! [
       "We strongly advise you encapsulate this instance inside a module,"
       "in order to isolate it from the rest of the code, and to be able"
       "to import it on demand. See the above paper and the file"
-      "https://github.com/math-comp/hierarchy-builder/blob/master/tests/non-forgetful-inheritance.v"
+      "https://github.com/math-comp/hierarchy-builder/blob/master/tests/non_forgetful_inheritance.v"
       "to witness devastating effects."
     ) true
 ].

HB/pack.elpi

@@ -14,7 +14,10 @@ main Ty Args Instance :- std.do! [
   get-constructor Class KC,
   get-constructor Structure KS,
 
-  std.assert-ok! (coq.elaborate-ty-skeleton TSkel _ T) "HB.pack: not a type",
+  std.assert-ok! (d\
+    (coq.elaborate-ty-skeleton TSkel _ T d, d = ok) ;
+     coq.elaborate-skeleton    TSkel _ T d
+  ) "HB.pack: not a well typed key",
 
   private.elab-factories FactoriesSkel T Factories,
 

Makefile.test-suite.coq.local

@@ -12,13 +12,15 @@ DIFF=\
 	$(COQTOP) $(COQFLAGS) $(COQLIBS) -topfile $(1) \
 	  < $(1) 2>/dev/null \
 	  | grep -v -e "Skipping rcfile" -e "is declared" -e "is defined" -e "Loading ML file" -e "Welcome to Coq" \
+	  | sed -E 's/characters? [0-9-]+://' \
 	  > $(1).out.aux;\
-	diff -u --strip-trailing-cr $(call output_for,$(1)) $(1).out.aux;\
+	wdiff $(call output_for,$(1)) $(1).out.aux;\
 	fi
 
 post-all::
 	$(call DIFF, tests/compress_coe.v)
 	$(call DIFF, tests/about.v)
+	$(call DIFF, tests/howto.v)
 	$(call DIFF, tests/missing_join_error.v)
 	$(call DIFF, tests/not_same_key.v)
 	$(call DIFF, tests/hnf.v)

README.md

@@ -82,7 +82,8 @@ Proof. by rewrite example. Qed.
 This [paper](https://hal.inria.fr/hal-02478907) describes the language
 in details, and the corresponding talk [is available on youtube](https://www.youtube.com/watch?v=F6iRaTlQrlo).
 The [wiki](https://github.com/math-comp/hierarchy-builder/wiki) gathers some
-tricks and FAQs.
+tricks and FAQs. If you want to work on the implementation of HB, this
+[recorded hacking session](https://www.youtube.com/watch?v=gmaJjCbzqO0) may be relevant to you.
 
 ### Installation & availability
 
@@ -150,6 +151,7 @@ opam install coq-hierarchy-builder
   - `HB.locate` is similar to `Locate`, prints file name and line of any global
     constant synthesized by HB
   - `HB.graph` prints the structure hierarchy to a dot file
+  - `HB.howto` prints sequences of factories to equip a type with a given structure
 
 - HB debug commands:
   - `HB.status` dumps the contents of the hierarchy (debug purposes)

_CoqProject.test-suite

@@ -52,6 +52,8 @@ examples/Coq2020_material/CoqWS_abstract.v
 examples/Coq2020_material/CoqWS_expansion/withHB.v
 examples/Coq2020_material/CoqWS_expansion/withoutHB.v
 
+examples/cat/cat.v
+
 tests/type_of_exported_ops.v
 tests/duplicate_structure.v
 tests/instance_params_no_type.v
@@ -63,12 +65,13 @@ tests/exports2.v
 tests/log_impargs_record.v
 tests/compress_coe.v
 tests/funclass.v
+tests/grefclass.v
 tests/local_instance.v
 tests/lock.v
 tests/interleave_context.v
 tests/not_same_key.v
 #tests/factory_sort.v
-tests/factory_sort_tac.v
+tests/hb_pack.v
 tests/declare.v
 tests/short.v
 tests/primitive_records.v

coq-hierarchy-builder-shim.opam

@@ -11,7 +11,7 @@ dev-repo: "git+https://github.com/math-comp/hierarchy-builder"
 build: [ make "-C" "shim" "build" ]
 install: [ make "-C" "shim" "install" ]
 conflicts: [ "coq-hierarchy-builder" ]
-depends: [ "coq" {>= "8.10"} ]
+depends: [ "coq-elpi" { (>= "1.14" & < "1.17~") | = "dev" } ]
 synopsis: "Shim package for HB"
 description: """
 This package provide the support constants one can use to compile files

coq-hierarchy-builder.opam

@@ -12,7 +12,7 @@ build: [ [ make "build"]
          [ make "test-suite" ] {with-test}
        ]
 install: [ make "install" ]
-depends: [ "coq-elpi" { (>= "1.15.1" & < "1.16~") | = "dev" } ]
+depends: [ "coq-elpi" { (>= "1.15.1" & < "1.17~") | = "dev" } ]
 conflicts: [ "coq-hierarchy-builder-shim" ]
 synopsis: "High level commands to declare and evolve a hierarchy based on packed classes"
 description: """

examples/hulk.v

@@ -258,6 +258,8 @@ Abort.
 
 End SlowFailure.
 
+(* cf https://github.com/coq/coq/issues/17223 *)
+Optimize Heap.
 
 Module FastFailure.
 

structures.v

@@ -252,14 +252,12 @@ Elpi Accumulate Db hb.db.
 #[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
 Elpi Accumulate lp:{{
 
-main _ :- coq.version _ _ N _, N < 13, !,
-  coq.say "HB: HB.locate requires Coq version 8.13 or above".
 main [str S] :- !,
   if (decl-location {coq.locate S} Loc)
      (coq.say "HB: synthesized in file" Loc)
      (coq.say "HB:" S "not synthesized by HB").
 
-main _ :- coq.error "Usage: HB.about <name>.".
+main _ :- coq.error "Usage: HB.locate <name>.".
 }}.
 Elpi Typecheck.
 Elpi Export HB.locate.
@@ -297,6 +295,53 @@ Elpi Typecheck.
 Elpi Export HB.about.
 
 
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+
+(** [HB.howto (T) Foo.type d] prints possible sequences of factories
+    to equip a type [T] with a structure [Foo.type], taking into account
+    structures already instantiated on [T]. The search depth [d]
+    is the maximum length of the sequences, 3 by default.
+    The first argument [T] is optional, when ommited [Foo.type] is built
+    from scratch.
+    Finally, the first argument can be another structure [Bar.type],
+    in which case [Foo.type] is built starting from [Bar.type].
+*)
+
+#[arguments(raw)] Elpi Command HB.howto.
+#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
+#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
+Elpi Accumulate File "HB/common/stdpp.elpi".
+Elpi Accumulate File "HB/common/database.elpi".
+Elpi Accumulate File "HB/common/utils.elpi".
+Elpi Accumulate File "HB/common/log.elpi".
+Elpi Accumulate File "HB/about.elpi".
+Elpi Accumulate File "HB/howto.elpi".
+Elpi Accumulate Db hb.db.
+Elpi Accumulate lp:{{
+
+main [trm T, str STgt] :- !,
+  with-attributes (with-logging (howto.main-trm T STgt none)).
+main [trm T, str STgt, int Depth] :- !,
+  with-attributes (with-logging (howto.main-trm T STgt (some Depth))).
+main [str T, str STgt] :- !,
+  with-attributes (with-logging (howto.main-str T STgt none)).
+main [str T, str STgt, int Depth] :- !,
+  with-attributes (with-logging (howto.main-str T STgt (some Depth))).
+main [str STgt] :- !,
+  with-attributes (with-logging (howto.main-from [] STgt none)).
+main [str STgt, int Depth] :- !,
+  with-attributes (with-logging (howto.main-from [] STgt (some Depth))).
+
+main _ :-
+  coq.error
+    "Usage: HB.howto [(<type>)|<structure>] <structure> [<search depth>].".
+}}.
+Elpi Typecheck.
+Elpi Export HB.howto.
+
+
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -532,7 +577,7 @@ HB.structure Definition StructureName params :=
   - [#[infer(variable)]], where [variable : pT] belongs to [params] and is a structure
     (e.g. from the hierarchy) with a coercion/canonical projection [pT >-> Sortclass].
     It modifies the notation [StructureName.type] so as to accept [variable : Type] instead,
-    and will try to infer it's [pT] by unification (using canonical structure inference),
+    and will try to infer its [pT] by unification (using canonical structure inference),
     This is essential in [Lmodule.type R] where [R] should have type [Ring.type]
     but any [Type] which is canonically a [Ring.type] is accepted thanks to [#[infer(R)]].
     If the carrier of the structure [S] is not a [Type] but rather a function, one has

tests/about.v

@@ -48,4 +48,11 @@ HB.about hierarchy_5_Ring__to__hierarchy_5_SemiRing.
 (* builder *)
 HB.about Builders_40.hierarchy_5_Ring_of_AddAG__to__hierarchy_5_BiNearRing_of_AddMonoid.
 
-HB.locate BinNums_Z__canonical__hierarchy_5_AddAG.
+HB.locate BinNums_Z__canonical__hierarchy_5_AddAG.
+
+(* Test minimally qualified names *)
+Module Import hierarchy_5.
+Module AddComoid.
+End AddComoid.
+End hierarchy_5.
+HB.about Z.

tests/about.v.out

@@ -8,13 +8,13 @@ HB: AddMonoid_of_TYPE operations and axioms are:
     - addr0
 HB: AddMonoid_of_TYPE requires the following mixins:
 HB: AddMonoid_of_TYPE provides the following mixins:
-    - hierarchy_5.AddMonoid_of_TYPE
+    - AddMonoid_of_TYPE
 
 HB: AddMonoid_of_TYPE.Build is a factory constructor
     (from "./examples/demo1/hierarchy_5.v", line 10)
 HB: AddMonoid_of_TYPE.Build requires its subject to be already equipped with:
 HB: AddMonoid_of_TYPE.Build provides the following mixins:
-    - hierarchy_5.AddMonoid_of_TYPE
+    - AddMonoid_of_TYPE
 HB: arguments: AddMonoid_of_TYPE.Build S zero add addrA add0r addr0
     - S : Type
     - zero : AddMonoid.sort S
@@ -27,33 +27,33 @@ HB: AddAG.type is a structure (from "./examples/demo1/hierarchy_5.v", line 73)
 HB: AddAG.type characterizing operations and axioms are:
     - addNr
     - opp
-HB: hierarchy_5.AddAG is a factory for the following mixins:
-    - hierarchy_5.AddMonoid_of_TYPE
-    - hierarchy_5.AddComoid_of_AddMonoid
-    - hierarchy_5.AddAG_of_AddComoid (* new, not from inheritance *)
-HB: hierarchy_5.AddAG inherits from:
-    - hierarchy_5.AddMonoid
-    - hierarchy_5.AddComoid
-HB: hierarchy_5.AddAG is inherited by:
-    - hierarchy_5.Ring
+HB: AddAG is a factory for the following mixins:
+    - AddMonoid_of_TYPE
+    - AddComoid_of_AddMonoid
+    - AddAG_of_AddComoid (* new, not from inheritance *)
+HB: AddAG inherits from:
+    - AddMonoid
+    - AddComoid
+HB: AddAG is inherited by:
+    - Ring
 
-HB: hierarchy_5.AddMonoid.type is a structure
+HB: AddMonoid.type is a structure
     (from "./examples/demo1/hierarchy_5.v", line 17)
-HB: hierarchy_5.AddMonoid.type characterizing operations and axioms are:
+HB: AddMonoid.type characterizing operations and axioms are:
     - addr0
     - add0r
     - addrA
     - add
     - zero
-HB: hierarchy_5.AddMonoid is a factory for the following mixins:
-    - hierarchy_5.AddMonoid_of_TYPE (* new, not from inheritance *)
-HB: hierarchy_5.AddMonoid inherits from:
-HB: hierarchy_5.AddMonoid is inherited by:
-    - hierarchy_5.AddComoid
-    - hierarchy_5.AddAG
-    - hierarchy_5.BiNearRing
-    - hierarchy_5.SemiRing
-    - hierarchy_5.Ring
+HB: AddMonoid is a factory for the following mixins:
+    - AddMonoid_of_TYPE (* new, not from inheritance *)
+HB: AddMonoid inherits from:
+HB: AddMonoid is inherited by:
+    - AddComoid
+    - AddAG
+    - BiNearRing
+    - SemiRing
+    - Ring
 
 HB: Ring_of_AddAG is a factory
     (from "./examples/demo1/hierarchy_5.v", line 108)
@@ -66,11 +66,11 @@ HB: Ring_of_AddAG operations and axioms are:
     - mulrDl
     - mulrDr
 HB: Ring_of_AddAG requires the following mixins:
-    - hierarchy_5.AddMonoid_of_TYPE
-    - hierarchy_5.AddComoid_of_AddMonoid
-    - hierarchy_5.AddAG_of_AddComoid
+    - AddMonoid_of_TYPE
+    - AddComoid_of_AddMonoid
+    - AddAG_of_AddComoid
 HB: Ring_of_AddAG provides the following mixins:
-    - hierarchy_5.BiNearRing_of_AddMonoid
+    - BiNearRing_of_AddMonoid
 Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and
      mul0r are derived from addrC and the other ring axioms, following a proof
      of Hankel (Gerhard Betsch. On the beginnings and development of near-ring
@@ -82,11 +82,11 @@ Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and
 HB: Ring_of_AddAG.Build is a factory constructor
     (from "./examples/demo1/hierarchy_5.v", line 108)
 HB: Ring_of_AddAG.Build requires its subject to be already equipped with:
-    - hierarchy_5.AddMonoid_of_TYPE
-    - hierarchy_5.AddComoid_of_AddMonoid
-    - hierarchy_5.AddAG_of_AddComoid
+    - AddMonoid_of_TYPE
+    - AddComoid_of_AddMonoid
+    - AddAG_of_AddComoid
 HB: Ring_of_AddAG.Build provides the following mixins:
-    - hierarchy_5.BiNearRing_of_AddMonoid
+    - BiNearRing_of_AddMonoid
 HB: arguments: Ring_of_AddAG.Build A [one] [mul] mulrA mulr1 mul1r mulrDl mulrDr
     - A : Type
     - one : A
@@ -104,9 +104,9 @@ Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and
      and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht,
      1995).
 
-HB: add is an operation of structure hierarchy_5.AddMonoid
+HB: add is an operation of structure AddMonoid
     (from "./examples/demo1/hierarchy_5.v", line 17)
-HB: add comes from mixin hierarchy_5.AddMonoid_of_TYPE
+HB: add comes from mixin AddMonoid_of_TYPE
     (from "./examples/demo1/hierarchy_5.v", line 10)
 
 HB: AddAG.sort is a canonical projection
@@ -116,27 +116,36 @@ HB: AddAG.sort has the following canonical values:
     - Ring.sort (from "./examples/demo1/hierarchy_5.v", line 196)
     - Z 
 
-HB: AddAG.sort is a coercion from hierarchy_5.AddAG to Sortclass
+HB: AddAG.sort is a coercion from AddAG to Sortclass
     (from "./examples/demo1/hierarchy_5.v", line 73)
 
-HB: Z is canonically equipped with mixins:
-    - hierarchy_5.AddMonoid
-      hierarchy_5.AddComoid
-      hierarchy_5.AddAG
+HB: Z is canonically equipped with structures:
+    - AddMonoid
+      AddComoid
+      AddAG
       (from "(stdin)", line 5)
-    - hierarchy_5.BiNearRing
-      hierarchy_5.SemiRing
-      hierarchy_5.Ring
+    - BiNearRing
+      SemiRing
+      Ring
       (from "(stdin)", line 10)
 
 HB: hierarchy_5_Ring_class__to__hierarchy_5_SemiRing_class is a coercion from
-    hierarchy_5.Ring to hierarchy_5.SemiRing
-    (from "./examples/demo1/hierarchy_5.v", line 196)
+    Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196)
 
 HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from
-    hierarchy_5.Ring to hierarchy_5.SemiRing
-    (from "./examples/demo1/hierarchy_5.v", line 196)
+    Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196)
 
-HB: todo HB.about for builder from hierarchy_5.Ring_of_AddAG to 
-hierarchy_5.BiNearRing_of_AddMonoid
+HB: todo HB.about for builder from Ring_of_AddAG to BiNearRing_of_AddMonoid
 HB: synthesized in file File "(stdin)", line 5, column 0, character 127:
+Interactive Module hierarchy_5 started
+Interactive Module AddComoid started
+HB: Z is canonically equipped with structures:
+    - AddMonoid
+      demo1.hierarchy_5.AddComoid
+      AddAG
+      (from "(stdin)", line 5)
+    - BiNearRing
+      SemiRing
+      Ring
+      (from "(stdin)", line 10)
+

tests/about.v.out.14 → tests/about.v.out.15

@@ -8,13 +8,13 @@ HB: AddMonoid_of_TYPE operations and axioms are:
     - addr0
 HB: AddMonoid_of_TYPE requires the following mixins:
 HB: AddMonoid_of_TYPE provides the following mixins:
-    - hierarchy_5.AddMonoid_of_TYPE
+    - AddMonoid_of_TYPE
 
 HB: AddMonoid_of_TYPE.Build is a factory constructor
     (from "./examples/demo1/hierarchy_5.v", line 10)
 HB: AddMonoid_of_TYPE.Build requires its subject to be already equipped with:
 HB: AddMonoid_of_TYPE.Build provides the following mixins:
-    - hierarchy_5.AddMonoid_of_TYPE
+    - AddMonoid_of_TYPE
 HB: arguments: AddMonoid_of_TYPE.Build S zero add addrA add0r addr0
     - S : Type
     - zero : AddMonoid.sort S
@@ -27,33 +27,33 @@ HB: AddAG.type is a structure (from "./examples/demo1/hierarchy_5.v", line 73)
 HB: AddAG.type characterizing operations and axioms are:
     - addNr
     - opp
-HB: hierarchy_5.AddAG is a factory for the following mixins:
-    - hierarchy_5.AddMonoid_of_TYPE
-    - hierarchy_5.AddComoid_of_AddMonoid
-    - hierarchy_5.AddAG_of_AddComoid (* new, not from inheritance *)
-HB: hierarchy_5.AddAG inherits from:
-    - hierarchy_5.AddMonoid
-    - hierarchy_5.AddComoid
-HB: hierarchy_5.AddAG is inherited by:
-    - hierarchy_5.Ring
+HB: AddAG is a factory for the following mixins:
+    - AddMonoid_of_TYPE
+    - AddComoid_of_AddMonoid
+    - AddAG_of_AddComoid (* new, not from inheritance *)
+HB: AddAG inherits from:
+    - AddMonoid
+    - AddComoid
+HB: AddAG is inherited by:
+    - Ring
 
-HB: hierarchy_5.AddMonoid.type is a structure
+HB: AddMonoid.type is a structure
     (from "./examples/demo1/hierarchy_5.v", line 17)
-HB: hierarchy_5.AddMonoid.type characterizing operations and axioms are:
+HB: AddMonoid.type characterizing operations and axioms are:
     - addr0
     - add0r
     - addrA
     - add
     - zero
-HB: hierarchy_5.AddMonoid is a factory for the following mixins:
-    - hierarchy_5.AddMonoid_of_TYPE (* new, not from inheritance *)
-HB: hierarchy_5.AddMonoid inherits from:
-HB: hierarchy_5.AddMonoid is inherited by:
-    - hierarchy_5.AddComoid
-    - hierarchy_5.AddAG
-    - hierarchy_5.BiNearRing
-    - hierarchy_5.SemiRing
-    - hierarchy_5.Ring
+HB: AddMonoid is a factory for the following mixins:
+    - AddMonoid_of_TYPE (* new, not from inheritance *)
+HB: AddMonoid inherits from:
+HB: AddMonoid is inherited by:
+    - AddComoid
+    - AddAG
+    - BiNearRing
+    - SemiRing
+    - Ring
 
 HB: Ring_of_AddAG is a factory
     (from "./examples/demo1/hierarchy_5.v", line 108)
@@ -66,11 +66,11 @@ HB: Ring_of_AddAG operations and axioms are:
     - mulrDl
     - mulrDr
 HB: Ring_of_AddAG requires the following mixins:
-    - hierarchy_5.AddMonoid_of_TYPE
-    - hierarchy_5.AddComoid_of_AddMonoid
-    - hierarchy_5.AddAG_of_AddComoid
+    - AddMonoid_of_TYPE
+    - AddComoid_of_AddMonoid
+    - AddAG_of_AddComoid
 HB: Ring_of_AddAG provides the following mixins:
-    - hierarchy_5.BiNearRing_of_AddMonoid
+    - BiNearRing_of_AddMonoid
 Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and
      mul0r are derived from addrC and the other ring axioms, following a proof
      of Hankel (Gerhard Betsch. On the beginnings and development of near-ring
@@ -82,11 +82,11 @@ Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and
 HB: Ring_of_AddAG.Build is a factory constructor
     (from "./examples/demo1/hierarchy_5.v", line 108)
 HB: Ring_of_AddAG.Build requires its subject to be already equipped with:
-    - hierarchy_5.AddMonoid_of_TYPE
-    - hierarchy_5.AddComoid_of_AddMonoid
-    - hierarchy_5.AddAG_of_AddComoid
+    - AddMonoid_of_TYPE
+    - AddComoid_of_AddMonoid
+    - AddAG_of_AddComoid
 HB: Ring_of_AddAG.Build provides the following mixins:
-    - hierarchy_5.BiNearRing_of_AddMonoid
+    - BiNearRing_of_AddMonoid
 HB: arguments: Ring_of_AddAG.Build A [one] [mul] mulrA mulr1 mul1r mulrDl mulrDr
     - A : Type
     - one : A
@@ -104,9 +104,9 @@ Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and
      and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht,
      1995).
 
-HB: add is an operation of structure hierarchy_5.AddMonoid
+HB: add is an operation of structure AddMonoid
     (from "./examples/demo1/hierarchy_5.v", line 17)
-HB: add comes from mixin hierarchy_5.AddMonoid_of_TYPE
+HB: add comes from mixin AddMonoid_of_TYPE
     (from "./examples/demo1/hierarchy_5.v", line 10)
 
 HB: AddAG.sort is a canonical projection
@@ -116,27 +116,36 @@ HB: AddAG.sort has the following canonical values:
     - Ring.sort (from "./examples/demo1/hierarchy_5.v", line 196)
     - Z 
 
-HB: AddAG.sort is a coercion from hierarchy_5.AddAG to Sortclass
+HB: AddAG.sort is a coercion from AddAG to Sortclass
     (from "./examples/demo1/hierarchy_5.v", line 73)
 
-HB: Z is canonically equipped with mixins:
-    - hierarchy_5.AddMonoid
-      hierarchy_5.AddComoid
-      hierarchy_5.AddAG
+HB: Z is canonically equipped with structures:
+    - AddMonoid
+      AddComoid
+      AddAG
       (from "(stdin)", line 5)
-    - hierarchy_5.BiNearRing
-      hierarchy_5.SemiRing
-      hierarchy_5.Ring
+    - BiNearRing
+      SemiRing
+      Ring
       (from "(stdin)", line 10)
 
 HB: hierarchy_5_Ring_class__to__hierarchy_5_SemiRing_class is a coercion from
-    hierarchy_5.Ring to hierarchy_5.SemiRing
-    (from "./examples/demo1/hierarchy_5.v", line 196)
+    Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196)
 
 HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from
-    hierarchy_5.Ring to hierarchy_5.SemiRing
-    (from "./examples/demo1/hierarchy_5.v", line 196)
+    Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196)
 
-HB: todo HB.about for builder from hierarchy_5.Ring_of_AddAG to 
-hierarchy_5.BiNearRing_of_AddMonoid
+HB: todo HB.about for builder from Ring_of_AddAG to BiNearRing_of_AddMonoid
 HB: synthesized in file File "(stdin)", line 5, column 122, character 127:
+Interactive Module hierarchy_5 started
+Interactive Module AddComoid started
+HB: Z is canonically equipped with structures:
+    - AddMonoid
+      demo1.hierarchy_5.AddComoid
+      AddAG
+      (from "(stdin)", line 5)
+    - BiNearRing
+      SemiRing
+      Ring
+      (from "(stdin)", line 10)
+

tests/grefclass.v

@@ -0,0 +1,12 @@
+From HB Require Import structures.
+
+Definition pred T := T -> bool.
+
+HB.mixin Record isPredNat (f : pred nat) := {}.
+
+HB.structure Definition PredNat := {f of isPredNat f}.
+
+Section TestSort.
+Variable p : PredNat.type.
+Check p : pred nat.
+End TestSort.

tests/factory_sort_tac.v → tests/hb_pack.v

@@ -25,7 +25,7 @@ About hasA'.type.
 
 Section test.
 Variables (G : Prop) (P : AB.type -> G).
-
+(* problem with planB
 Goal forall T (a b : T), G.
 Proof.
 move=> T a b.
@@ -35,7 +35,7 @@ pose Tab := hasB.Build A (b,b).
 pose AB : AB.type := ltac:(elpi HB.pack (A) (Tab)).
 exact: P AB.
 Qed.
-
+*)
 Goal forall T (a b : T), G.
 Proof.
 move=> T a b.
@@ -111,4 +111,15 @@ pose X := Foo.pack T (HasFoo.Build A P T H).
 Check X : Foo.type A P.
 Abort.
 
-End test2.
+End test2.
+
+HB.mixin Record isID T (F : T -> T) := { p : forall x : T, F x = x }.
+HB.structure Definition Fun T := { F of isID T F }.
+
+Goal forall f : nat -> nat, forall p : (forall x, f x = x ), True.
+intros f p.
+pose F := isID.Build nat f p.
+pose T : Fun.type nat := HB.pack f F.
+Check T : Fun.type nat.
+Abort.
+

tests/howto.v

@@ -0,0 +1,33 @@
+From Coq Require Import ZArith ssrfun ssreflect.
+From HB Require Import structures.
+From HB Require Import demo1.hierarchy_5.
+
+HB.howto Ring.type.
+
+HB.howto Ring.type 2.
+
+HB.howto Z Ring.type.
+
+HB.howto Z Ring.type 2.
+
+Fail HB.howto Z Ring.type 0.
+
+HB.howto AddComoid.type Ring.type.
+
+HB.instance
+  Definition _ :=
+  AddAG_of_TYPE.Build Z 0%Z Z.add Z.opp
+    Z.add_assoc Z.add_comm Z.add_0_l Z.add_opp_diag_l.
+
+HB.howto Z Ring.type.
+
+HB.howto AddAG.type Ring.type.
+
+HB.instance
+  Definition _ :=
+  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.
+
+HB.howto Z Ring.type.

tests/howto.v.out

@@ -0,0 +1,55 @@
+HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
+    - Ring_of_TYPE
+    - AddAG_of_TYPE; BiNearRing_of_AddMonoid
+    - AddAG_of_TYPE; Ring_of_AddAG
+    - AddAG_of_TYPE; SemiRing_of_AddComoid
+    - AddComoid_of_TYPE; Ring_of_AddComoid
+    - AddComoid_of_TYPE; AddAG_of_AddComoid; BiNearRing_of_AddMonoid
+    - AddComoid_of_TYPE; AddAG_of_AddComoid; Ring_of_AddAG
+    - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid
+    - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid
+
+HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
+    - Ring_of_TYPE
+    - AddAG_of_TYPE; BiNearRing_of_AddMonoid
+    - AddAG_of_TYPE; Ring_of_AddAG
+    - AddAG_of_TYPE; SemiRing_of_AddComoid
+    - AddComoid_of_TYPE; Ring_of_AddComoid
+
+HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
+    - Ring_of_TYPE
+    - AddAG_of_TYPE; BiNearRing_of_AddMonoid
+    - AddAG_of_TYPE; Ring_of_AddAG
+    - AddAG_of_TYPE; SemiRing_of_AddComoid
+    - AddComoid_of_TYPE; Ring_of_AddComoid
+    - AddComoid_of_TYPE; AddAG_of_AddComoid; BiNearRing_of_AddMonoid
+    - AddComoid_of_TYPE; AddAG_of_AddComoid; Ring_of_AddAG
+    - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid
+    - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid
+
+HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
+    - Ring_of_TYPE
+    - AddAG_of_TYPE; BiNearRing_of_AddMonoid
+    - AddAG_of_TYPE; Ring_of_AddAG
+    - AddAG_of_TYPE; SemiRing_of_AddComoid
+    - AddComoid_of_TYPE; Ring_of_AddComoid
+
+The command has indeed failed with message:
+HB: no solution found, try to increase search depth.
+HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
+    - Ring_of_AddComoid
+    - AddAG_of_AddComoid; BiNearRing_of_AddMonoid
+    - AddAG_of_AddComoid; Ring_of_AddAG
+    - AddAG_of_AddComoid; SemiRing_of_AddComoid
+
+HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
+    - BiNearRing_of_AddMonoid
+    - Ring_of_AddAG
+    - SemiRing_of_AddComoid
+
+HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
+    - BiNearRing_of_AddMonoid
+    - Ring_of_AddAG
+    - SemiRing_of_AddComoid
+
+HB: nothing to do.

tests/infer.v

@@ -17,7 +17,7 @@ HB.mixin Record barm (A : Type) (P : foo.type) (B: Type) (T : Type) := {
 HB.structure Definition bar A P B := { T of barm A P B T }.
 
 #[skip="8.1[0-5].*"] HB.check (bar.type_ bool nat bool).
-#[skip="8.16.*", fail] HB.check (bar.type_ bool nat bool).
+#[skip="8.1[6-9].*", fail] HB.check (bar.type_ bool nat bool).
 Print bar.phant_type.
 Print bar.type.
 Check bar.type bool nat bool.

tests/interleave_context.v

@@ -7,9 +7,12 @@ HB.structure Definition A n := { T of HasA n T }.
 HB.mixin Record HasB (X : A.type 0) (T : Type) := { b : X -> T }.
 HB.structure Definition B (X : A.type 0) := { T of HasB X T }.
 
-#[verbose]
+(* Since `B` expects an argument of type `A.type 0` (and not just
+   just the naked type `T`) we pass `A.clone 0 T _`
+   (of type `A.type 0`) and inference uses the first
+   parameter `A` to elaborate it. *)
 HB.mixin Record IsSelfA T of A 0 T & B (A.clone 0 T _) T := {}.
-#[verbose]
+
 HB.structure Definition SelfA := { T of IsSelfA T }.
 
 HB.factory Record IsSelfA' T := { a : T ; b : T -> T}.
@@ -19,5 +22,4 @@ HB.builders Context T of IsSelfA' T.
   HB.instance Definition _ := IsSelfA.Build T.
 HB.end.
 
-#[verbose]
-  HB.instance Definition _ := IsSelfA'.Build nat 0 id.
+HB.instance Definition _ := IsSelfA'.Build nat 0 id.

tests/rev_coerce.v

@@ -0,0 +1,24 @@
+From HB Require Import structures.
+
+HB.mixin Record isPointed V := { point : V }.
+HB.structure Definition Pointed := {V of isPointed V}.
+
+Definition popt (U : Pointed.type) := option U.
+HB.instance Definition _ U := isPointed.Build (popt U) None.
+
+HB.mixin Record hasTrue (U V : Pointed.type) (f : U -> V) := {
+  true_subproof : True
+}.
+HB.structure Definition HasTrue (U V : Pointed.type) := {f of hasTrue U V f}.
+
+Definition poptp (U : Pointed.type) (p : popt U) : U := point.
+
+Section Bug.
+Variable U : Pointed.type.
+
+Check hasTrue.Build (popt U) U (@poptp U) I.
+Set Printing Universes.
+(* There used to be a universe issue at the line below: *)
+HB.instance Definition _ := hasTrue.Build (popt U) U (@poptp U) I.
+
+End Bug.