Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
1 result
Blame Permalink
Forked from Iris / Iris
Source project has a limited visibility.
  • Ralf Jung's avatar
    0540c073
    Relax subG mode · 0540c073
    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
    History
    Relax subG mode
    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) Σ)