search

coq / vscoq

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

Changing `Require Import` Stops Highlighting #745

Closed joscoh closed 7 months ago

joscoh commented 7 months ago

I am running VSCoq 2.1.0 on manual mode (Coq 8.18.0). I have the following (test) file:

Require Import Coq.Lists.List.

Definition foo := nat.

Print nat.

Definition size {A: Type} (l: list A) : nat :=
  List.fold_right (fun x acc => 1 + acc) 0 l.

I can use VSCoq as usual. However, if I comment out the Require Import, there is no more green highlighting. I know that the proof checking is still happening in the background, since the Print command still gets underlined blue. But there is no more highlighting. Moreover, there is no highlighting in any other file either until I close VSCode and reload.

rtetley commented 7 months ago

Hey ! Thanks for reporting ! I am unable to reproduce in version 2.1.2 ! Could you check and let me know ?

joscoh commented 7 months ago

Seems to be fixed after upgrading to 2.1.2. Thanks!

rtetley commented 7 months ago

Cool :-) I'll go ahead and close this then !