Coq

Originally proposed by @charguer as part of #10559 as:

• The command Open HintDb mybase. loads mybase over the current section/module, meaning that eauto implicitly means eauto with mybase.

~~I personally have my doubts on the Open HintDb syntax because I find it too close to the Open Scope command and therefore likely to make users think that its effects are cumulative (you coul

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.