coq-tools icon indicating copy to clipboard operation
coq-tools copied to clipboard

Minimizer: try to split <+ into Include

Open SkySkimmer opened this issue 2 years ago • 1 comments

Typically Module Foo args := A <+ B is the same as

Module Foo args.
Include A.
Include B.
End Foo.

SkySkimmer avatar Mar 16 '23 15:03 SkySkimmer

This should be pretty easy with a regex.

JasonGross avatar Mar 16 '23 16:03 JasonGross