Yves Bertot
With the following file as playground. ``` Require Import List Reals. Open Scope R_scope. Definition fib_aux := nat_rect (fun _ => list R) (0 :: 1 :: nil) (fun _...
In the attached picture the formatting of the last n - 2 is weird. 
I have been tinkering with various versions of vscoq, but now I don't manage to get back into a working context. It seems code does not use the version of...
`Inspect .` is supposed to display n elements, like the results of `Search`. If one puts an `Inspect` command in the middle of the script, the results is displayed in...
When Search returns a theorem with a huge statement, some parts of the theorem are ellided, but hovering over the ellipsis should give some hint on how to expand the...