want to use just `fct_ringType` from topology.v

[t6s]

There is a ringType decaration for function types in topology.v, which I have recently found useful for some projects (namely affeldt-aist/infotheo and ieva-itu/robustmean) with no topology.

Unfortunately, importing topology conflicts with Morphism from Coq standard library which reserves the notation --> differently. I have to do some dirty coding to avoid this problem.

Could this be solved perhaps by separating the ring declaration out of topology.v? (Or perhaps by changing the reserved notation -->?)

[affeldt-aist]

It has been pointed out during the last mca meeting that a new feature of Coq (https://coq.inria.fr/refman/language/core/modules.html#grammar-token-import_categories) could help you solve this issue (by preventing loading of the conflicting notation). If it works for you, we can maybe avoid splitting topology.v for now and close this issue. What do you think? (No hurry.)

[proux01]

@affeldt-aist this issue seem to be fixed now as fct_ringType is now in the classical package (in functions.v). @t6s do you confirm?

[t6s]

Yes.