Adding parameters to HB.

- introduced w-params A and w-args A, with combinators
  w-params.then, w-params.map and list-w-params.flatten-map
- replaced `toposort-1` by `toposort-proj triple_1`

Co-Authored-By: Cyril Cohen <cyril.cohen@inria.fr>
Co-Authored-By: Kazuhiko Sakaguchi <pi8027@gmail.com>

.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,21 @@
+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.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.