In my code I enable primitive projections and redefine prod like the following:

`Record prod A B := pair { fst: A ; snd: B }.`

Full code theories/Defaults.v · master · Molly Stewart-Gallus / Category Fun · GitLab

I need this sort of weirdness because pattern matching on an inductive type has weird behavior. Without this change:

`Definition tupleprod '(A, B): Type := A * B.`

Has different inference than

`Definition tupleprod X: Type := fst X * snd X.`

I assume there are good reasons but Coq does not evaluate

```
let '(a, b) := ab in
a * b
```

to

`(let '(a, b) := ab in a) * (let '(a, b) := ab in b)`

Commonly this sort of thing is a problem with functors and heavily dependently typed code.

I assume similar issues might arise with existentials and the subset type but I haven’t run into any yet. Also if I redefine those then I break use of the Program plugin.

Anyhow I just wanted to ask if there was a nicer way of doing this sort of thing and if anyone else has encountered similar issues.

I was also curious exactly how backwards incompatible such a change would be. I know I ran into a few minor issues already.