GitLab

iSpecialize (("HLT" with "Hg") with "HL"). fails with

Error:
In nested Ltac calls to "iSpecialize (open_constr)", "iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)" and
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)", last call failed.
Tactic failure: iSpecialize: ("HLT" with "Hg") should be a hypothesis, use iPoseProof instead.

While that's technically true, it seems unfortunate, and forces me to call two tactics for the job. I end up writing iSpecialize ("HLT" with "Hg"); iDestruct ("HLT" with "HL") as "#HLT1"; auto. instead of iDestruct (("HLT" with "Hg") with "HL") as "#HLT1"; auto., which fails with

Error:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"iDestructCore (open_constr) as (constr) (tactic)", "iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic)", "iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
"<iris.proofmode.ltac_tactics.iPoseProofCore_go>" and "<iris.proofmode.ltac_tactics.iIntoEmpValid>", last call
failed.
No applicable tactic.

FWIW here's my context. Things are persistent as I'm not yet using mutable state (only persistent ghost state).

1 subgoal (ID 3041)
  
  Σ : gFunctors
  HdotG : dotG Σ
  Γ : list ty
  T, L, U : ty
  γ : gname
  ρ : vls
  l : label
  v : vl
  ============================
  "Hv" : γ ⤇ (λ ρ0 : leibnizC vls, ⟦ T ⟧ ρ0)
  "Hg" : ⟦ Γ ⟧* ρ
  "HLU" : ∀ (ρ0 : leibnizC vls) (v0 : vl), ⟦ Γ ⟧* ρ0 → ⟦ L ⟧ ρ0 v0 → ⟦ U ⟧ ρ0 v0
  "HTU" : ∀ (ρ0 : leibnizC vls) (v0 : vl), ⟦ Γ ⟧* ρ0 → ▷ ⟦ T ⟧ ρ0 v0 → ▷ ⟦ U ⟧ ρ0 v0
  "HLT" : ∀ (ρ0 : leibnizC vls) (v0 : vl), ⟦ Γ ⟧* ρ0 → ▷ ⟦ L ⟧ ρ0 v0 → ▷ ⟦ T ⟧ ρ0 v0
  "HL" : ▷ ⟦ L ⟧ ρ v
  --------------------------------------□
  ▷ □ ⟦ T ⟧ ρ v