Adapt to Coq PR #17084: maximal implicit arguments now added to references in defined Ltac code - #30

Adapt to Coq PR #17084: maximal implicit arguments now added to references in defined Ltac code#30

herbelin wants to merge 1 commit into

rocq-community:masterrocq-community/autosubst:masterfrom

herbelin:master+adapt-pr17084-align-strict-interpretation-of-references-on-non-strict-modeherbelin/autosubst:master+adapt-pr17084-align-strict-interpretation-of-references-on-non-strict-modeCopy head branch name to clipboard