Interactive mode to complete instances in tactics mode#595

Open

cecilemarcon wants to merge 16 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

Commits on Apr 30, 2026

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

Commits on May 11, 2026

working with pr 1010 of elpi
cecilemarcon
committed

Commits on Jun 4, 2026

Commits on Jun 5, 2026

naming of constants in instances
cecilemarcon
committed