adapt to mc#1256

[Tragicus]

Motivation for this change

math-comp/math-comp#1256 defines some structures on dependent function types, which requires a few rewrites (for things that do not unfold automatically) and annotations (to convince the unification algorithm).
There is bad interaction with tvs.v. When I have R : numFieldType, I can check that R is a topologicalType and a zmodType, but not a TopologicalZmodule.type, and when I try to make HB compute the missing instances, it complains about non_forgetful_inheritance.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[proux01]

The title / commit message says mc#1169 but the top message mentions mc#1256 ?

[Tragicus]

I can not change the name of the branch, so let's pretend that it has the right name, all the rest should be fixed.

[Tragicus]

I removed the instances on dependent functions from math-comp/math-comp#1256. There is only a bad interaction with tvs left. When I have R : numFieldType, I can check that R is a topologicalType and a zmodType, but not a TopologicalZmodule.type, and when I try to make HB compute the missing instances, it complains about non_forgetful_inheritance.