Relax subG mode
Compare changes
+ 1
− 1
@@ -87,7 +87,7 @@ search is only triggered if the arguments of [subG] do not contain evars. Since
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) Σ)