Issue to post to the Coq bug tracker asking to fill the survey

[Zimmi48]

Here is a proposal to review:

---

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 coq/coq#14740 (direct survey link)
• Understand some inductive cumulativity in old unification  coq/coq#14758 (direct survey link)
• Default HintDb option coq/coq#14777 (direct survey link)
• Remove 8.13 deprecations coq/coq#14819 (direct survey link)

@SkySkimmer:

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

@ana-borges:

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

@herbelin:

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

@mattam82:

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

@maximedenes:

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

@mrhaandi:

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

@olaure01:

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

@ppedrot:

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

@proux01:

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