-
Ralf Jung authored
With Coq master, we otherwise fail to infer instances with subG_savedAnythingΣ, which leads to goals like > looking for (subG > (@savedAnythingΣ (@ofe_funCF val (fun _ : val => laterCF idCF)) > ?cFunctorContractive0) Σ)
0540c073
With Coq master, we otherwise fail to infer instances with subG_savedAnythingΣ, which leads to goals like > looking for (subG > (@savedAnythingΣ (@ofe_funCF val (fun _ : val => laterCF idCF)) > ?cFunctorContractive0) Σ)