Merge pull request #1154 from MetaCoq/cherry-picks-on-9.0

Cherry picks on 9.0

Special case for dune

Remove autogenerated file from VCS

Merge pull request #1117 from 4ever2/eta-expand-app-fix

Fix substitution during eta expansion of partial application

Fix erasure_live_test

Proof that reordering of constructors is correct (#1095)

* WIP on reordering constructors

* New/old tag reasoning

* WIP correctness of constructor reordering. main lemma proven

* Reordering preserves well-formedness

* Reorderin

* Admit free proofs of preservation for wf and substitution

* WIP adapting to an additional mapping argument for transforms and stronger wellformedness property on extracted terms

* Full composed pipeline with mapping of constructors

* Fixes due to removal of useless -fast flag and change for reordering of constructors, now verified

* Remove option to reorder constructors, now safely done always

* Fix metacoq_tour

* Fix a remaining todo

* Remove generated files

Fix after merge

Fix script due to misclassification of implicit arg as potential type…

…class instance

Merge pull request #1068 from MetaCoq/fix-1042

Fix issue #1042 MetaCoq Run does not support evars.

Merge pull request #1065 from MetaCoq/fix-typo

Fix typo