Interactive mode to complete instances in tactics mode - #595

Open

cecilemarcon wants to merge 19 commits into

math-comp:masterfrom

cecilemarcon:interactive-mode

Commits on Apr 28, 2026

version of the code that allows to make interactive proofs without parameters
cecilemarcon
committed
02f9da5

Commits on Apr 29, 2026

Commits on Apr 30, 2026

can handle multiple interactive goals through product: todo, split automatically
cecilemarcon
committed
b1b0c17
handles multiple interactive goals, still has to better handle context
cecilemarcon
committed
e75473d

Commits on May 11, 2026

working with pr 1010 of elpi
cecilemarcon
committed
6b54131

Commits on Jun 4, 2026

changes with Enrico
cecilemarcon
committed
bccd67e
commented some lines because of bug introduced in instance
cecilemarcon
committed
f52ca78
wip, idk what are the types
cecilemarcon
committed
97926f2

Commits on Jun 5, 2026

naming of constants in instances
cecilemarcon
committed
1b1bdca

Commits on Jun 8, 2026

Commits on Jul 27, 2026

small commit
cecilemarcon
committed
efe90c6
moved code to utils
cecilemarcon
committed
e3ab630