diff options
| author | Erik Martin-Dorel | 2019-12-27 00:13:52 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-12-27 00:30:26 +0100 |
| commit | ec2d1bc0d0f0447f8824def545697b8c05fcb670 (patch) | |
| tree | f120e755c0c0cf09919874288dfb3335f8de0a24 /kernel/nativecode.mli | |
| parent | 4c19baf3a1b0ee9b1e94df4bca29c53125445db8 (diff) | |
fix: Shorten ssrsetoid.v
* This patch is a quick fix that removes part of the features of coq/coq#10022,
namely the ability to directly use setoid_rewrite with a (Under_rel)-tagged
relation R. This just means we'll need to do an extra step [rewrite UnderE.]
which was unnecessary with Coq 8.11+alpha.
* This PR stays backward-compatible w.r.t. Coq 8.10 and also keeps the salient
feature of coq/coq#10022 (generalize under & over to any Reflexive relation).
* Related: coq-community/atbr#23
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions