Making `Theorem with` more flexible + code cleanup - #18743

Merged

coqbot-app[bot] merged 6 commits into

rocq-prover:masterfrom

herbelin:master+more-flexible-theorem-with

May 16, 2024

Commits on May 15, 2024

Removing overly strong restriction in tactic "fix".
herbelin
committed
f671bb2
Support in search_guard for checking both if a fix or a cofix + simplifications

herbelin
and
SkySkimmer
committed
5b90d5d
Simplifying "Theorem with" and making it more flexible.
herbelin
committed
8c05b0b
Overlay for equations
herbelin
committed
c099ea8
Treating possible guard the same in the 3 functions declaring mutual definitions.
herbelin
committed
ae777ef
Change log for #18743
herbelin
committed
79d2443