aboutsummaryrefslogtreecommitdiff
path: root/test-suite/ltac2/constr.v
AgeCommit message (Expand)Author
2019-09-24Fix #10783: use binder_annot in Ltac2.Constr.Unsafe.kindGaƫtan Gilbert