Search results

Trocq Use accepts wrong term

bugSomething isn't workingSomething isn't working

Status: Open.

Bug

#78 In rocq-community/trocq;

· MysaaJava opened on Apr 16, 2026

Trocq interaction with sections

bugSomething isn't workingSomething isn't working

Status: Open.

Bug

#77 In rocq-community/trocq;

· MysaaJava opened on Apr 16, 2026

Trocq Interface Rework

enhancementNew feature or requestNew feature or request

Status: Open.

Feature

#76 In rocq-community/trocq;

· MysaaJava opened on Apr 9, 2026

Trocq not working with monomorphic universes

bugSomething isn't workingSomething isn't working

Status: Open.

Bug

#75 In rocq-community/trocq;

· MysaaJava opened on Apr 8, 2026

Support for every Rocq terms

enhancementNew feature or requestNew feature or request

Status: Open.

Feature

#72 In rocq-community/trocq;

· MysaaJava opened on Apr 1, 2026

Add an Elpi Diagnosis

dev-enhancementImprovement of the codebaseImprovement of the codebase

Status: Open.

Feature

#68 In rocq-community/trocq;

· MysaaJava opened on Mar 4, 2026

Long Qed in examples/std/int_to_Zp.v

Status: Open.

#47 In rocq-community/trocq;

· t6s opened on May 19, 2025

Examples of CoqEAL style refinement

Status: Open.

#40 In rocq-community/trocq;

· palmskog opened on Jan 16, 2025

Automated class inference fault when using Trocq Use

bugSomething isn't workingSomething isn't working

UIUser interface of the pluginUser interface of the plugin

Status: Open.

#32 In rocq-community/trocq;

· ecranceMERCE opened on Jan 23, 2024

Predicate naming in constraint graph

documentationImprovements or additions to documentationImprovements or additions to documentation

invalidThis doesn't seem rightThis doesn't seem right

Status: Open.

#31 In rocq-community/trocq;

· ecranceMERCE opened on Jan 19, 2024

Duplicate code getting parametricity classes

documentationImprovements or additions to documentationImprovements or additions to documentation

invalidThis doesn't seem rightThis doesn't seem right

Status: Open.

#30 In rocq-community/trocq;

· ecranceMERCE opened on Jan 19, 2024

Adapt and use HB to generate Trocq relational structures

dependenciesCompatibility with other packagesCompatibility with other packages

enhancementNew feature or requestNew feature or request

Status: Open.

#28 In rocq-community/trocq;

· CohenCyril opened on Jan 18, 2024