Is there any good reason why

```
let X := type of t in
match goal with
| [ H : X |- _ ] => simpl
end
```

should fail for `t`

a term in the context?

Having this weird problem right now and wondering if it's a bug.

test.v

isolated the error as much as possible

```
The Coq Proof Assistant, version 8.15.1
compiled with OCaml 4.11.1
```

`coq-hott.8.15`

can't reproduce on master

sounds like https://github.com/coq/coq/issues/15554

Last updated: Jun 25 2024 at 18:02 UTC