Store types with a CS instance in Elpi's Db

[gares]

• add a new predicate in the Elpi Db in structures.v
  • in HB.instance generate and accumulate a new clause (see acc-clauses)

different approach, subsumes the former, but needs more thinking:

• (to be reviewed) also store the mixin-src clasues from pred declare-canonical-instances-from-factory (currently dropped)
  • deduce the list of types for which we can synthesize structure from mixin-src T _ _

Tutorial: https://github.com/LPCIC/coq-elpi/blob/master/examples/example_data_base.v
API Doc: https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi#L1651