1行に複数のtacticがあると、1つ目のtacticの実行結果しかでない

ryuta-ito / coqtop-vim

Interact with coqtop within Vim

0 stars 0 forks source link

Closed ryuta-ito closed 6 years ago

ryuta-ito commented 6 years ago

Lemma test : 1 = 1 -> 1 = 1.
Proof.
  intro. reflexivity.
Qed.

でintro. reflexivity.の行にgotoすると

No more subgoals.

ではなく

1 subgoal (ID 6)

  H : 1 = 1
  ============================
  1 = 1

となる