List view

Doc strings on hover

enhancementNew feature or requestNew feature or request

prio:high

Status: Open.

#990 In rocq-prover/vsrocq;

· rtetley opened on Jan 20, 2025

[feature] ability to interrupt Coq

enhancementNew feature or requestNew feature or request

prio:high

Status: Open.

#373 In rocq-prover/vsrocq;

· maximedenes opened on Feb 13, 2023

Export API for running tactics at a given loc

enhancementNew feature or requestNew feature or request

Status: Open.

#996 In rocq-prover/vsrocq;

· rtetley opened on Jan 20, 2025

Allow folding of Proofs and Sections

enhancementNew feature or requestNew feature or request

prio:high

Status: Open.

#137 In rocq-prover/vsrocq;

· Arkhist opened on May 23, 2020

Add support for folding ranges

enhancementNew feature or requestNew feature or request

prio:high

Status: Open.

#799 In rocq-prover/vsrocq;

· rtetley opened on Jun 26, 2024

Query in Error state

bugSomething isn't workingSomething isn't working

prio:high

Status: Open.

#607 In rocq-prover/vsrocq;

· rtetley opened on Sep 4, 2023

[vscoq2] Integrated search tool in proof view

enhancementNew feature or requestNew feature or request

prio:high

Status: Open.

#659 In rocq-prover/vsrocq;

· thery opened on Oct 11, 2023

manual proof mode should never result in a state where "There are no more subgoals" but Qed claims there are remaining open goals

bugSomething isn't workingSomething isn't working

Status: Open.

#1058 In rocq-prover/vsrocq;

· JasonGross opened on Mar 3, 2025