> You have something like that in Coq/ex/indent.v.
> I dream of a smie with two grammars (and lexers): one for first lines of
> commands and one inside commands. It would greatly simplify things I think.
I don't really know how to define "first lines" and "inside", but you
can definitely have
I'd go with any large file in the source distribution of Coq. In fact, a good
test might be to clone the Coq repo, reindent the whole standard library, check
these changes in, then reindent again with your changes and look at the git
diff. I expect the standard library + the Coq test suite to
I have a few tentative changes to coq-smie.el.
Does someone have some kind of test-suite somewhere against which I can
run my new code to try and avoid regressions?
Ideally, it should be fully automated, including fixing my bugs and
outputting a Coq proof that the result is correct, but I'll