[feature] parameters in structures

.travis/docker-install.sh

@@ -1,7 +1,5 @@
 #!/usr/bin/env bash
-
 set -e
-
 docker pull coqorg/coq:${COQ}
 docker run -d -i --init --name=COQ -v ${TRAVIS_BUILD_DIR}:/home/coq/${CONTRIB_NAME} -w /home/coq/${CONTRIB_NAME} coqorg/coq:${COQ}
 docker exec COQ /bin/bash --login -c "

.travis/docker-test.sh

@@ -1,7 +1,5 @@
 #!/usr/bin/env bash
-
 set -e
-
 echo -e "${ANSI_YELLOW}Building ${CONTRIB_NAME}...${ANSI_RESET}" && echo -en 'travis_fold:start:script\\r'
 
 docker exec COQ /bin/bash --login -c "

_CoqProject

@@ -29,6 +29,8 @@ demo3/test_0_0.v
 demo3/test_1_0.v
 demo3/test_2_0.v
 
+demo4/hierarchy_0.v
+
 FSCD2020_material/V1.v
 FSCD2020_material/V2.v
 FSCD2020_material/V3.v

demo4/hierarchy_0.v

@@ -0,0 +1,27 @@
+From HB Require Import structures.
+
+HB.mixin Record m1 (T : Type) (A : Type) := {
+  inhab : A;
+  inhab_param : T;
+}.
+HB.structure Definition s1 T := { A of m1 T A }.
+
+Check inhab.
+  (* inhab : forall (T : Type) (A : s1.type T), s1.sort A *)
+
+HB.instance Definition nat_m1 := m1.Build bool nat 7 false.
+Check (refl_equal _ : @inhab _ _ = 7).
+
+HB.instance Definition list_m1 A := m1.Build (option A) (list nat) (cons 7 nil) None.
+Check (refl_equal _ : @inhab _ _ = (cons 7 nil)).
+
+HB.mixin Record m2 (T : Type) (A : Type) of m1 T A := {
+  inj : T -> A;
+}.
+
+HB.structure Definition s2 T :=
+  { A of m1 T A & m2 T A }.
+
+Check fun X : s2.type nat => inhab : X.
+Check fun X : s2.type nat => inj : nat -> X.
+About s2_to_s1.