diff options
Diffstat (limited to 'test-suite/bugs/closed/3584.v')
| -rw-r--r-- | test-suite/bugs/closed/3584.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3584.v b/test-suite/bugs/closed/3584.v index 3d4660b4..37fe4637 100644 --- a/test-suite/bugs/closed/3584.v +++ b/test-suite/bugs/closed/3584.v @@ -13,4 +13,4 @@ Definition sum_of_sigT A B (x : sigT (fun b : bool => if b then A else B)) | existT _ false b => inr b end. (* Toplevel input, characters 0-182: Error: Pattern-matching expression on an object of inductive type sigT -has invalid information. *)
\ No newline at end of file +has invalid information. *) |