Mentioning incompatibility shown in #3718 and coming from #3050
(interpreting "match goal"'s hypotheses in scope %type).