diff options
Diffstat (limited to 'test-suite/bugs/opened/HoTT_coq_062.v')
| -rw-r--r-- | test-suite/bugs/opened/HoTT_coq_062.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_062.v b/test-suite/bugs/opened/HoTT_coq_062.v index 6c0221479..99c2a1fb5 100644 --- a/test-suite/bugs/opened/HoTT_coq_062.v +++ b/test-suite/bugs/opened/HoTT_coq_062.v @@ -70,8 +70,8 @@ Theorem thm `{Univalence} : (forall A, ((A -> False) -> False) -> A) -> False. intro f. Set Printing Universes. Set Printing All. - pose proof (apD f (path_universe e)). - pose proof (apD f p). + Fail pose proof (apD f (path_universe e)). + Fail pose proof (apD f p). (* Toplevel input, characters 18-19: Error: In environment |