Search results

VsCoq Legacy not working with rocq dev + compat layer?

Status: Open.

#1013 In coq/vscoq;

· mattam82 opened on Jan 28, 2025

Vscoq language server constantly crashing with "Unbound value Control.refine"

bugSomething isn't workingSomething isn't working

duplicateThis issue or pull request already existsThis issue or pull request already exists

Status: Open.

Bug

#1010 In coq/vscoq;

· JasonGross opened on Jan 25, 2025

Vscoq language server constantly crashing (probably, by bad syntax parsing?)

bugSomething isn't workingSomething isn't working

Status: Open.

Bug

#1009 In coq/vscoq;

· nirshahar opened on Jan 24, 2025

 ·  

Next release (v2.2.4)

extra space in \in display

bugSomething isn't workingSomething isn't working

Status: Open.

Bug

#1006 In coq/vscoq;

· gares opened on Jan 23, 2025

version 2.2.3 is a pre-release?

Status: Open.

#1005 In coq/vscoq;

· thery opened on Jan 23, 2025

Support for "Set Printing All / Set Printing Universes"

enhancementNew feature or requestNew feature or request

Status: Open.

Feature

#1004 In coq/vscoq;

· mattam82 opened on Jan 23, 2025

Parsing no longer seems to use vos files

bugSomething isn't workingSomething isn't working

Status: Open.

Bug

#1000 In coq/vscoq;

· tchajed opened on Jan 20, 2025

Consider adding configuration to expand all goals by default

enhancementNew feature or requestNew feature or request

Status: Open.

Feature

#999 In coq/vscoq;

· booleancoercion opened on Jan 20, 2025

Export API for running tactics at a given loc

enhancementNew feature or requestNew feature or request

Status: Open.

Feature

#996 In coq/vscoq;

· rtetley opened on Jan 20, 2025

 ·  

Next release (v2.2.4)

One click install

enhancementNew feature or requestNew feature or request

prio:high

Status: Open.

Feature

#994 In coq/vscoq;

· rtetley opened on Jan 20, 2025

 ·  

Road map star issues

Command: Search in coq documentation

enhancementNew feature or requestNew feature or request

prio:high

Status: Open.

Feature

#993 In coq/vscoq;

· rtetley opened on Jan 20, 2025

 ·  

Road map star issues

Hover in the goal view

enhancementNew feature or requestNew feature or request

prio:high

Status: Open.

Feature

#992 In coq/vscoq;

· rtetley opened on Jan 20, 2025

 ·  

Road map star issues