search

coq / vscoq

Visual Studio Code extension for Coq
MIT License
335 stars 68 forks source link

cleanup(EM): delegated tasks are executable sentences #916

Closed gares closed 2 weeks ago

gares commented 2 weeks ago

If an opaque proof contained as Skip (i.e. a syntax error) it was not delegated anyway by the scehduler.

I'm rebasing #915 on top of this one since it makes is much cleaner.

@rtetley please have a look at the code for id_of_first/last_task. I think my new code is equivalent, but I don't get in which cases the default would be different than the computed one.

rtetley commented 2 weeks ago

If I remember correctly, the opener and closer referred to the first proof step. This often lead us to not treat the Proof. or Qed. lines when coloring in delegation mode ?