Replacing (fun x => ...^~x) by the more readable [rel x y | ... y x] breaks real closed

[hivert]

We should investigate why using [rel x y | e x z] in path breaks real closed.

Originally posted by @chdoc in math-comp/math-comp#788 (review)

[ggonthier]

One likely explanation is that (fun x => eˆ~ x), i.e., (fun x y => e y x), is a unification pattern and will thus match any relation whatsoever without unfolding anything (beyond what is needed to expose the two head funs). While rep_of_simpl [rel x y | e y x] is convertible to this pattern, it is not syntactically a pattern itself and may thus cause some additional unfolding of constants.

[hivert]

Thanks @ggonthier for the analysis. In math-comp/math-comp#788 (comment), I was suggested to replace (fun x => eˆ~ x) by the more readable [rel x y | e y x]. From what you says here, I gather that this is not a so good idea, and that (fun x y => e y x) should be used instead. Can you confirm that ?