Relax subG mode
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) Σ)
Please register or sign in to comment