Non-fresh identifiers in intro patterns sometimes turn the goal unprovable instead of generating an error message
On latest Iris master (Coq 8.16.1), I am encountering the following error:
From iris Require Import base.
From iris.heap_lang Require Import proofmode.
Local Lemma bla `{!heapGS Σ} :
(True : iProp Σ) -∗
(True ∗ True) -∗ True.
Proof.
iIntros "Ha Hc".
iDestruct "Hc" as "(%Ha & Ha)".
(* goal becomes False *)
Abort.
It seems like the check for freshness sometimes fails to generate an error message.
Changing the second line of the proof script to iDestruct "Hc" as "(Hd & Ha)".
correctly generates an error message.