Slow compilation of fixpoints

[addap]

Hi,
I tried around with pathological cases and it seems the bigger the strongly connected components of sorts get, Coq has a hard time of figuring out which arguments of a mutually recursive fixpoint are structurally decreasing (at least in wellscoped code since there are more arguments to check). That's why I added an annotation to all the fixpoints.
I tested it with the attached language that has components of size 6. The wellscoped code takes around 30s to compile and with the annotation only 3s.

    Time |  Peak Mem | File Name                    
----------------------------------------------------
0m37.21s | 486628 ko | Total Time / Peak Mem        
----------------------------------------------------
0m29.44s | 486628 ko | test_6_3_wellscoped.vo       
0m02.91s | 389764 ko | test_6_3_wellscoped_struct.vo
0m02.66s | 381540 ko | test_6_3_unscoped.vo         
0m01.81s | 377196 ko | test_6_3_unscoped_struct.vo  
0m00.19s | 272656 ko | fintype.vo                   
0m00.11s | 183916 ko | axioms.vo                    
0m00.10s | 161228 ko | unscoped.vo                  

As a quick fix I just added the "{struct s}" text when printing since the name is always the same. But you might want to extract the name based on its position in the binders.

It's only two lines so here is a small patchfile
struct.patch