[Subsumed] Towards a single code path for the "using" clause + small improvement of "using Type" for co/fixpoints - #18742

[Subsumed] Towards a single code path for the "using" clause + small improvement of "using Type" for co/fixpoints#18742

herbelin wants to merge 4 commits into

rocq-prover:masterrocq-prover/rocq:masterfrom

herbelin:master+one-copy-of-using-clauseherbelin/github-coq:master+one-copy-of-using-clauseCopy head branch name to clipboard