Ssreflect Users Discussion List

[Florent Hivert <>]

      Dear all,

This is maybe a newbie question... As far as I remember, the printing of union
was working correctly, but in one of my file it now prints as

\big[setU (T:=tuple_finType (d1 + d2) (ordinal_finType n))/set0]_(Q in 
LRsupport)

While this is not critical, this becomes really annoying when there are 
several
nested union printed on the screen. I've no idea where to start to debug the
problem. Any pointer or suggestion ?

Cheers,

Florent


In case someone really want to reproduce the problem (on never knows ;-) :

siteswap-~/src/Coq/Combi $ coqc --version 
The Coq Proof Assistant, version 8.8.1 (August 2018)
compiled on Aug 18 2018 17:58:21 with OCaml 4.03.0

Installed with opam:
coq-mathcomp-algebra      1.7.0       Mathematical Components Library on 
Algebra
coq-mathcomp-bigenough    1.0.0       A small library to do epsilon - N 
reasonning.
coq-mathcomp-character    1.7.0       Mathematical Components Library on 
character t
coq-mathcomp-field        1.7.0       Mathematical Components Library on 
Fields
coq-mathcomp-fingroup     1.7.0       Mathematical Components Library on 
finite grou
coq-mathcomp-finmap       1.0.0       Finite sets, finite maps, finitely 
supported f
coq-mathcomp-multinomials 1.1         A Multinomial Library for the 
Mathematical Com
coq-mathcomp-odd-order    1.7.0
coq-mathcomp-solvable     1.7.0       Mathematical Components Library on 
finite grou
coq-mathcomp-ssreflect    1.7.0       Small Scale Reflection

As usual I'm working on

https://github.com/hivert/Coq-Combi/commit/bbfa0264e0ee6b5504cc83cf3b256cd601c91762

It appear for example in the file theories/LRrule/freeSchur.v in the proof of
free_LR_rule