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. P
Le sam. 1 déc. 2018 à 16:24, Stefan Monnier <monn...@iro.umontreal.ca> a écrit : > 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 settle for > a long file that I need to reindent&check manually. > > So far I have the coq/indent.v but it doesn't seem to include some cases > that are mentioned in coq-smie.el, so I'm hoping someone has something > a bit more complete. > > > Stefan > _______________________________________________ > ProofGeneral-devel mailing list > ProofGeneral-devel@inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel >
_______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
