Add a kludgy implementation of tmTry#876

JasonGross wants to merge 1 commit intoMetaRocq:coq-8.16MetaRocq/metarocq:coq-8.16from

JasonGross:coq-8.16+tmTry-hackJasonGross/metacoq:coq-8.16+tmTry-hackCopy head branch name to clipboard