aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/4354.v
AgeCommit message (Expand)Author
2015-10-09Refine fix for handling of the universe contexts of hints, depending onMatthieu Sozeau
2015-10-06Fix bug #4354: interpret hints in the right env and sigma.Matthieu Sozeau