aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3267.v
AgeCommit message (Collapse)Author
2018-10-04rename test files (do not start by a digit)Vincent Laporte
2015-10-29Fixing another instance of bug #3267 in eauto, this time in theHugo Herbelin
presence of hints modifying the context and of a "using" clause. Incidentally opening Hints by default in debugger.
2014-06-26Properly refresh the local hintdb database in case an external tactic changedMatthieu Sozeau
the hypotheses in eauto.