Skip to content

Set `Hint Mode` for `inG`.

Robbert Krebbers requested to merge ci/robbert/hintmode_inG into master

There was no Hint Mode for inG yet, causing Coq to pick arbitrary instances sometimes.

This MR uses the mode - for Σ since there is always a unique Σ. It uses the mode ! for A since we can have multiple inGs for different As, so we do not want Coq to pick one arbitrarily.

Class inG (Σ : gFunctors) (A : cmraT) :=
  InG { inG_id : gid Σ; inG_prf : A = gFunctors_lookup Σ inG_id (iPrePropO Σ) _ }.
Hint Mode inG - ! : typeclass_instances.

Merge request reports