add comments about STLC's use of irisGS being odd

theories/logrel/stlc/fundamental.v

@@ -10,6 +10,9 @@ Definition log_typed `{irisGS stlc_lang Σ}
 Notation "Γ ⊨ e : τ" := (log_typed Γ e τ) (at level 74, e, τ at next level).
 
 Section typed_interp.
+  (** STLC is somewhat unusual in that we quantify over an arbitrary [irisGS] --
+  almost all languages need to have a specific [irisGS] instance to fix their
+  specific [state_interp], but STLC has no state so it does not care. *)
   Context `{irisGS stlc_lang Σ}.
 
   Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) constr(Hp) :=

theories/logrel/stlc/logrel.v

@@ -9,6 +9,9 @@ Reserved Notation "⟦ Γ ⟧*" (at level 0, Γ at level 70).
 
 (** interp : is a unary logical relation. *)
 Section logrel.
+(** STLC is somewhat unusual in that we quantify over an arbitrary [irisGS] --
+almost all languages need to have a specific [irisGS] instance to fix their
+specific [state_interp], but STLC has no state so it does not care. *)
 Context `{irisGS stlc_lang Σ}.
 
 Fixpoint interp (τ : type) (w : val) : iProp Σ :=

theories/logrel/stlc/rules.v

@@ -6,6 +6,9 @@ From stdpp Require Import fin_maps.
 From iris.prelude Require Import options.
 
 Section stlc_rules.
+  (** STLC is somewhat unusual in that we quantify over an arbitrary [irisGS] --
+  almost all languages need to have a specific [irisGS] instance to fix their
+  specific [state_interp], but STLC has no state so it does not care. *)
   Context `{irisGS stlc_lang Σ}.
   Implicit Types e : expr.