Request feedback on the CI minimizer

[Zimmi48]

Hello, we (@JasonGross, @Zimmi48 and @achlipala) are trying to evaluate how useful the new CI minimization feature of coqbot is in practice. For that, we have created a very short survey (and most questions are optional) and we would appreciate if you could answer it for each pull request where the CI minimizer was used (that you authored or where you triggered the minimizer). Thanks a lot for your help!

Here is a list of pull requests for which we would appreciate your answer to the survey:

@Alizter:

• Split Scheme Equality into own vernac + misc cleanup #14740 (direct survey link)
• Understand some inductive cumulativity in old unification  #14758 (direct survey link)
• Default HintDb option #14777 (direct survey link)
• Remove 8.13 deprecations #14819 (direct survey link)

@SkySkimmer:

• Automatic bidirectionality hints #13107 (direct survey link)
• Fix handling of StuckClass in recursive typeclass search #14480 (direct survey link)
• Check typability of the "cut formula" before trying first order heuristic on second-order unification problems #14733 (direct survey link)
• Understand some inductive cumulativity in old unification  #14758 (direct survey link)
• CI: VST uses master branch #14783 (direct survey link)
• Use Cases to implement "let (x, y) := ..." instead of adhoc implem #14785 (direct survey link)
• Occur-check modulo the equivalence generated by evar-evar unification problems #14929 (direct survey link)
• Fix setoid_rewrite under non dependent binders #14986 (direct survey link)
• Fix coercions from projections #15048 (direct survey link)

@ana-borges:

• Rename Int63 ~> Uint63 #13895 (direct survey link)

@herbelin:

• Adding support for recursive blocs and associativity in ARGUMENT EXTEND #12743 (direct survey link)
• Occur-check modulo the equivalence generated by evar-evar unification problems #13126 (direct survey link)
• Let solve_simple_eqn be aware of the possibility to recover from an occur-check error by reasoning up to eta #13269 (direct survey link)
• Attribute to define namespace policy for an inductive type #14492 (direct survey link)
• Explicit Projection nodes in concrete syntax #14598 (direct survey link)
• Ad hoc fix for #12298: flushing defined Ltac evars in tactical abstract #14671 (direct survey link)
• Check typability of the "cut formula" before trying first order heuristic on second-order unification problems #14733 (direct survey link)
• Add a criterion to decide when a cyclic evar instantiation is actually valid #14746 (direct survey link)
• Add support for extracting subterms of invertible constructors in unification #14798 (direct survey link)
• Occur-check modulo the equivalence generated by evar-evar unification problems #14929 (direct survey link)

@mattam82:

• Fix bug #7916, allowing Reflexive to have mode ! ! #13969 (direct survey link)
• Do not consider scrutinees of projections and cases as heads for hint mode "!" #14392 (direct survey link)

@maximedenes:

• Do not call unification heuristics before resolving TC #13072 (direct survey link)

@mrhaandi:

• Less forceful preprocessing for congruence #14612 (direct survey link)

@olaure01:

• [stdlib] Add properties and predicates on lists with output in Type #11966 (direct survey link)

@ppedrot:

• Non-global terms declared as hints now generate a proxy constant. #12493 (direct survey link)
• "auto using *" now poses its arguments #12512 (direct survey link)
• Store the closedness of a term on its leave in unification matchrec. #14253 (direct survey link)
• More uniform handling of variable patterns in Btermdn. #14722 (direct survey link)
• More principled implementation of Btermdnet matching #14788 (direct survey link)
• Uniformly use dnets for goals with evars in all auto tactics #14848 (direct survey link)

@proux01:

• Parameters of inductives in Number Notations can be arbitrary terms #14818 (direct survey link)
• Remove 8.13 deprecations #14819 (direct survey link)