diff options
Diffstat (limited to 'test-suite/bugs/closed/3513.v')
| -rw-r--r-- | test-suite/bugs/closed/3513.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v index ff515038e..9ed0926a6 100644 --- a/test-suite/bugs/closed/3513.v +++ b/test-suite/bugs/closed/3513.v @@ -89,5 +89,6 @@ Debug: 2.2.1.1.1.1: apply ILFun_ILogic on (ILogic OPred) Show Existentials. Set Typeclasses Debug Verbosity 2. Set Printing All. - Fail apply reflexivity. + (* As in 8.5, allow a shelved subgoal to remain *) + apply reflexivity.
\ No newline at end of file |