Skip to content

GitLab

Closed
Created by Robbert Krebbers@robbertkrebbersMaintainer

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?