aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_11046.v
AgeCommit message (Expand)Author
2019-11-05Fixing test-suiteKenji Maillard
2019-11-04Prevent double definition of Ltac2 constructors inside a module; Fix #11046Kenji Maillard