aboutsummaryrefslogtreecommitdiff
path: root/test-suite/ltac2/notations.v
AgeCommit message (Expand)Author
2019-06-06[Ltac2] Interpretation scopes in “constr” arguments of tactic notationsVincent Laporte