Search results

[FEAT] Cannot install dev version of vsrocq-language-server without a local clone of the repository

bugSomething isn't workingSomething isn't working

Status: Open.

#1230 In rocq-prover/vsrocq;

· bn-peters opened on Apr 9, 2026

[BUG] > Print does nothing

bugSomething isn't workingSomething isn't working

Status: Open.

#1225 In rocq-prover/vsrocq;

· mattam82 opened on Mar 26, 2026

[FEAT] Interface for other VSCode Extensions

enhancementNew feature or requestNew feature or request

Status: Open.

#1222 In rocq-prover/vsrocq;

· caldwellb opened on Mar 24, 2026

[BUG] Crash when trying to close a section with an open goal that defines a notation

bugSomething isn't workingSomething isn't working

Status: Open.

#1221 In rocq-prover/vsrocq;

· KacperFKorban opened on Mar 20, 2026

✨ Set up Copilot instructions

Status: Open.

#1215 In rocq-prover/vsrocq;

· gares opened on Mar 7, 2026

[BUG] Set Silent and -quiet have no effect

bugSomething isn't workingSomething isn't working

Status: Open.

#1210 In rocq-prover/vsrocq;

· cpitclaudel opened on Feb 16, 2026

[FEAT] Report Rocq version

enhancementNew feature or requestNew feature or request

Status: Open.

#1209 In rocq-prover/vsrocq;

· cpitclaudel opened on Feb 15, 2026

[FEAT] Perhaps the reset (︽) command should restart vsrocq entirely?

enhancementNew feature or requestNew feature or request

Status: Open.

#1207 In rocq-prover/vsrocq;

· cpitclaudel opened on Feb 15, 2026

[FEAT] Add a blocking request to check that parsing is complete

enhancementNew feature or requestNew feature or request

Status: Open.

#1206 In rocq-prover/vsrocq;

· cpitclaudel opened on Feb 15, 2026

[FEAT] Provide a structured, complete view of the whole document in one query

enhancementNew feature or requestNew feature or request

Status: Open.

#1205 In rocq-prover/vsrocq;

· cpitclaudel opened on Feb 15, 2026

[BUG] Diagnostic range is wrong

bugSomething isn't workingSomething isn't working

Status: Open.

#1204 In rocq-prover/vsrocq;

· cpitclaudel opened on Feb 15, 2026

[BUG] Warnings are delayed until further input

bugSomething isn't workingSomething isn't working

Status: Open.

#1203 In rocq-prover/vsrocq;

· cpitclaudel opened on Feb 15, 2026