Emilio Jesús Gallego Arias

Oh no! I guess there is some automated tool that would check this. I'll fix ASAP, feel free to remove that file, it is just an example.

@herbelin , indeed testing this stuff is hard and I didn't realize of the real problem until later (which also impacted coq-lsp, which I have to say has no issues...

@herbelin the standard method for positions these days is indeed line / column , encoded in very different ways tho, due to windows and unicode (actually I misinterpreted the LSP...

> I confirm (and I have no idea a priori of how to fix it). What the rest of the code does is to adjust the locations, I guess this...

> You mean an http link? Or a copy of the sources? Anyway, we can discuss it elsewhere. A symlink to a copy of the sources, or just drop a...

I second @herbelin point, that indeed it would be helpful to produce better error messages in situations that are not supported. When developing this happens often, for example, I recently...

IMO we need to be a bit bold here, it doesn't seem sensible to me that we keep shipping `abstract` in their current state. cc: @JasonGross as an abstract power...

> Abstract is this side effect stuff right? It does a bit more than that, but basically yes. > I don't really understand how it works though. In many cases,...

> I think that `transparent_abstract` is also an important tactic. It shares a lot of code with `abstract`, and is more tunable Sure @JasonGross , for the purposes of this...

> Maybe abstract shouldn't be adding constants during the proof but only at the end. During the proof we just log that there is an effect `x : A :=...