blob: 431123ec1b36af85115a6a1e37804150e70099ff (
plain)
1
2
3
4
5
6
|
- **Fixed:**
``Program Fixpoint`` now uses ``ex`` and ``sig`` to make telescopes
involving ``Prop`` types (`#10758
<https://github.com/coq/coq/pull/10758>`_, by Gaëtan Gilbert, fixing
`#10757 <https://github.com/coq/coq/issues/10757>`_ reported by
Xavier Leroy).
|
