Search results

Bug: Error not being caught in Expand function

Status: Open.

Bug

#215 In impermeable/coq-waterproof;

· jim-portegies opened on Nov 16, 2025

Bug: Expand definitions leading to "Not_focussed" error

Status: Open.

Bug

#214 In impermeable/coq-waterproof;

· jim-portegies opened on Nov 16, 2025

Both directions and Structural Induction

Status: Open.

#209 In impermeable/coq-waterproof;

· SebLhye opened on Nov 13, 2025

Assume ... yields unexpected behaviour

Status: Open.

#208 In impermeable/coq-waterproof;

· pimotte opened on Nov 11, 2025

Doc: Syntax update process

Status: Open.

#198 In impermeable/coq-waterproof;

· pimotte opened on Oct 30, 2025

Allow teachers to remove alternative characterizations and definitions

Status: Open.

#197 In impermeable/coq-waterproof;

· jim-portegies opened on Oct 27, 2025

Add deregistration for unfold/alternative characterization

Status: Open.

#195 In impermeable/coq-waterproof;

· pimotte opened on Oct 23, 2025

spike: Investigate and fix notation levels

Status: Open.

#186 In impermeable/coq-waterproof;

· pimotte opened on Oct 2, 2025

It holds that P cannot be removed before We conclude that P

good first issueGood for newcomersGood for newcomers

Status: Open.

#171 In impermeable/coq-waterproof;

· jcommelin opened on Aug 25, 2025

Support multiple statements in It holds that.

good first issueGood for newcomersGood for newcomers

Status: Open.

#169 In impermeable/coq-waterproof;

· pimotte opened on Aug 15, 2025

Bug: Feedback for proving "/\ False"

bugSomething isn't workingSomething isn't working

good first issueGood for newcomersGood for newcomers

Status: Open.

Bug

#166 In impermeable/coq-waterproof;

· pimotte opened on Aug 7, 2025

Use goal naming to improve feedback

Status: Open.

#158 In impermeable/coq-waterproof;

· pimotte opened on Jun 26, 2025