Pierre Courtieu
Pierre Courtieu
Hi, is this solved?
Would you expect that when you type something just after the locked region (with no separating space) it would behave as if the last dot of the region was edited?...
Isn't it the `dune` file that we want to detect here? `dune-project` is not necessary is it? Be careful, we use the _CoqProject informations for other actions than just launching...
OK and no other feature of company-coq needs the compile-options?
@hendriktews this seems to ne easy to rebase. Is there any reason not to?
> > The reason is that rewrite xyz by tactic (without the dot) is also valid, and that could reasonably be considered to need indentation. > > I don't understand...
Yes. It is a known bug however since The user can interrupt Coq and fix the missing space it is an acceptable behavior imho, although not perfect.
Thanks for reporting. I will have a look at it. Interestingly the timing is not put inside ``. Another workaround is to switch off tidy response: `(setq proof-tidy-response nil)`.
I think this feature goes beyong ssreflect. I have been thinking about something like this for the `;` tactical. Debuging `foo;bar;rab;oof` boils down to the same mechanics really. My 2...
@chdoc, @erikmd good points. This complex parsing of commands is probably much easier and safer to code on the ocaml side. @chdoc I don't understand your remark about the document...