Proof mode goals in empty context cannot be distinguished from Coq goals
@jung noted this problem somewhere in lambdarust, see below for a simple example:
From iris Require Import proofmode.tactics.
Goal forall M (P : uPred M), P ⊣⊢ P.
Proof.
intros; iSplit.
(* Goals look like `P → P` *)We could add some special symbol to the proof mode notation with the empty context? Any suggestions?