affeldt-aist

> the fix is quite trivial Ok. Since there is a number of definitions that are added to `contra.v` and many canonicals, it didn't look trivial to me ^_^. >...

There is certainly something smarter to do with `R^c`.

@CohenCyril Since you thumbs uped the corresponding you may have an interest in this PR. Otherwise, we'll postpone to 1.0.0.

`mulr_rev` definition unfolded, as discussed during the last MathComp-Analysis dev meeting.

Ok, it looks like the HB.instance for the `R^c` case is of no use in MathComp-Analysis...

I check and report asap.

and what about if we need to make the measure explicit? `{ae[mu], f =1 g}` ? (If we need to make both the measure and the support set explicit, then...

Maybe we should have defined ```coq Definition ae_eq f g := {ae mu, forall x, D x -> f x = g x}. ``` as ```coq Definition ae_eq f g...

Thanks. This also makes (minor) generalizations clearer. While playing around with the topological definitions, I also observed the following one: issue #1042 now PRed in PR #1043

As discussed during the last meeting, we are planning to merge this PR. Before we merge, @chdoc could you test that `graph-theory` still compiles with this PR? (Since `graph-theory` requires...