How to deal with `emp`, `True`, and friends when the BI is ambigious
The following discussion from !115 (merged) should be addressed:
We often write emp : PROP
. However, since coercions are explicit term constructors in Coq, this apparently leads to unification problems here and there.
The alternative is to write bi_emp (PROP:=PROP)
, which is ugly.
Maybe we should have special notations to force the type arguments of emp
, True
, and friends.
I think ssr is also doing something like that. Depending on the outcome of this issue, we should not just address the occurrence in !115 (merged), but also fix other occurrences.
Edited by Robbert Krebbers