Adapt to Coq PR #17084: maximal implicit arguments now added to references in defined Ltac code#30
Open
herbelin wants to merge 1 commit intocoq-community:masterfrom herbelin:master+adapt-pr17084-align-strict-interpretation-of-references-on-non-strict-mode
+2-2
