universes : bool; | Should we print hidden sort quality variables? |
qualities : bool; |
relevances : bool; | If true, prints full local context of evars |
evar_instances : bool; |
wildcard : bool; |
fast_names : bool; |
synth_match_return : bool; |
matching : bool; |
primproj_params : bool; |
unfolded_primproj_as_match : bool; |
match_paramunivs : bool; |
always_regular_match_style : bool; |
nonpropositional_letin_types : bool; |