diff options
Diffstat (limited to 'test-suite/bugs/opened/HoTT_coq_107.v')
| -rw-r--r-- | test-suite/bugs/opened/HoTT_coq_107.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_107.v b/test-suite/bugs/opened/HoTT_coq_107.v index c3a83627e..f8b595d85 100644 --- a/test-suite/bugs/opened/HoTT_coq_107.v +++ b/test-suite/bugs/opened/HoTT_coq_107.v @@ -70,7 +70,7 @@ Definition trunc_sum' n A B `{IsTrunc n Bool, IsTrunc n A, IsTrunc n B} Proof. Set Printing All. Set Printing Universes. - refine (@trunc_sigma Bool (fun b => if b then A else B) n _ _). + Fail refine (@trunc_sigma Bool (fun b => if b then A else B) n _ _). (* Toplevel input, characters 23-76: Error: In environment |