Commit 9774b1ec authored by Ralf Jung's avatar Ralf Jung

Merge branch 'ralf/subg' into 'master'

Relax subG mode

See merge request iris/iris!255
parents eeeda7c0 0540c073
......@@ -87,7 +87,7 @@ search is only triggered if the arguments of [subG] do not contain evars. Since
instance search for [subG] is restrained, instances should persistently have [subG] as
their first parameter to avoid loops. For example, the instances [subG_authΣ]
and [auth_discrete] otherwise create a cycle that pops up arbitrarily. *)
Hint Mode subG + + : typeclass_instances.
Hint Mode subG ! + : typeclass_instances.
Lemma subG_inv Σ1 Σ2 Σ : subG (gFunctors.app Σ1 Σ2) Σ subG Σ1 Σ * subG Σ2 Σ.
Proof.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment