-
Robbert Krebbers authored
This ensures compatiblity with https://github.com/coq/coq/pull/10762, it also allows us to get rid of the weird `id` hack in `iIntoEmp`. On the flipside, in some cases unification now fails. But it seems to involve HO-unification problems, where it has to solve `?Φ x` for some evar `Φ`. IMHO, it is mystery to me why this worked before...
59b24ea7