missing qualid in extracted env dataset

[Desperatesonic]

when examining the file "Free_module.v" in coq_project "algebra", I found that some qualid data (e.g. 'eqFMd_op_assoc') in the tactics (e.g. 'exact eqFMd_op_assoc') could not be found in the extracted env dataset(I tried to search it from all the qualid or short ident in the env or hypothesis ).
by further examination, I found that there was a inductive type eqFMd defined between 'num_extra_cmds'(which is 131) and 'line_nb' of the first proofdata (which is 143), I guess this is the source of the problem. did something go wrong when extracting env? I am not so sure about it. Maybe this discovery is useful for the community when someone tries to do the premise selection like me.

[Desperatesonic]

oh, I made a mistake, actually these qualids could be found in the blocks of inductives of env.

[Desperatesonic]

Just got a statistics about the QUALID type arguments in tactics (359655) grouping by where they could be found:
'in_Sertop_cons': 47840, # all QUALID data belong to constants of Sertop
'in_Sertop_inducs': 157, # all QUALID data belong to inductives of Sertop
'in_hypothesis': 169886, # all QUALD data belong to hypothesis of the goals
'in_inductives': 0, # all QUALD data belong to QUALID in inductives' blocks
'in_inductives_constructors': 2076, # all QUALD data belong to constructors in inductives' blocks
'in_inductives_short': 1636, # all QUALD data belong to short ident in inductives' blocks
'in_qualid': 2, # all QUALD data belong to QUALID in constants of env
'in_short': 149181, # all QUALD data belong to short ident in constants of env
'not_in_all': 24530, # could not be found
'': 14061, # all QUALID equal to ''
'not_in_hypothesis': 189769,
'not_in_inductives': 359655,
'not_in_inductives_constructors': 357579,
'not_in_inductives_short': 358019,
'not_in_qualid': 359653,
'not_in_short': 210474}