I'm getting this warning everywhere and there is no information in the warning (or, as far as I can tell, in the documentation) of how to actually declare something local, global, or export. https://coq.inria.fr/refman/proofs/automatic-tactics/auto.html#grammar-token-hint_info has no information and https://coq.inria.fr/refman/language/core/modules.html#coq:attr.local tells me that there is

There is now a type circle in UniMath.SyntheticHomotopyTheory.Circle2. It would be great to define pi_1 of a pointed type, and to show that pi_1(circle, pt) \simeq Z.

I've noticed that even with the fastest reduction strategy available - lazy - running tmEval within the TemplateMonad is still much slower than vm_compute. I have an example for which tmEval lazy takes around 22 sec, and vm_compute finishes in 4.5 sec.

Is there a way of using vm_compute for reduction?

Characters like (space) are not allowed for .v files, but vscoq does not give any useful error message and just hangs if accidently called on such files. Same for file names with empty name (filename just .v, happens occasionally when i hit some shortcut by accident).

Eval cbn in 1 + 1.
Definition x :=
  Eval cbn in 1 + 1.
Definition y := 2.

The second Eval is not highlighted, and the second Definition is indented to match the second Eval.