There is a Coq-community project that works fine in 8.17 but fails in Coq 8.18 with a "Error: setoid rewrite failed". Are there any changes other than PR 17304 related to `setoid_rewrite`

that may be the culprit? I tried searching the release notes but didn't see anything else obvious.

This is the error message, which may or may not help:

```
File "./theories/libs/sltype.v", line 145, characters 33-59:
Error:
setoid rewrite failed: Unable to satisfy the following constraints:
UNDEFINED EVARS:
?X1876==[form ssub decompP F ssub_F
(LF:=[fset C in powerset F | literalC C]) C IH inU s inC nL S S1
S2 S3 S4 |- Relation_Definitions.relation form]
(internal placeholder) {?r}
?X1877==[form ssub decompP F ssub_F
(LF:=[fset C in powerset F | literalC C]) C IH inU s inC nL S S1
S2 S3 S4 |- Relation_Definitions.relation form]
(internal placeholder) {?r0}
?X1878==[form ssub decompP F ssub_F
(LF:=[fset C in powerset F | literalC C]) C IH inU s inC nL S S1
S2 S3 S4 (do_subrelation:=Morphisms.do_subrelation) |-
Morphisms.Proper
(Morphisms.respectful
(fun x y : form =>
(let (T, mprv, Imp, _, _, _) as m return (m -> Prop) :=
let (msort, Bot', _) := slp_form form in msort in
mprv) (x <--> y)) (Morphisms.respectful ?r0 ?r))
(Imp_op (m:=form))] (internal placeholder) {?p}
?X1879==[form ssub decompP F ssub_F
(LF:=[fset C in powerset F | literalC C]) C IH inU s inC nL S S1
S2 S3 S4 |- Morphisms.ProperProxy ?r0 (\or_(D<-base LF C) [af D])]
(internal placeholder) {?p0}
?X1880==[form ssub decompP F ssub_F
(LF:=[fset C in powerset F | literalC C]) C IH inU s inC nL S S1
S2 S3 S4 (do_subrelation:=Morphisms.do_subrelation) |-
Morphisms.Proper
(Morphisms.respectful ?r (Basics.flip Basics.impl))
(mprv (m:=form))] (internal placeholder) {?p1}
TYPECLASSES:?X1876 ?X1877 ?X1878 ?X1879 ?X1880
SHELF:||
FUTURE GOALS STACK:?X1880 ?X1879 ?X1878 ?X1877 ?X1876||
```

Last updated: Oct 13 2024 at 01:02 UTC