vscoq2.1.3 big output breaks display of goal

[ybertot]

The following code displays correctly for small values of fib (up to 11) and breaks starting at (12). What breaks is that the goal window is empty. Normal behavoir can only by restored by entering "Developer:Reload Window".

Require Import List Reals.
Open Scope R_scope.

Definition fib_aux :=
  nat_rect (fun _ => list R) (0 :: 1 :: nil)
    (fun _ v => (nth 1 v 0 :: nth 0 v 0 + nth 1 v 0 :: nil))
.

Definition fib (n : nat) : R :=
  nth 0 (fib_aux n) 0.

Lemma big_fib : fib 12 = 10.
Proof.
unfold fib; simpl.

[ybertot]

It seems I made a mistake and fib 12 does not provoke the problem, rather fib 14 should be used. But it is still quite a small number.

Here is another example, which is more representative of a real programming activity:

Require Import List Reals Lia.
Open Scope R_scope.

Definition fib_aux :=
  nat_rect (fun _ => list R) (0 :: 1 :: nil)
    (fun _ v => (nth 1 v 0 :: nth 0 v 0 + nth 1 v 0 :: nil))
.

Lemma nat_rect_step (B : nat -> Type) (v0 : B O)
  (stp : forall n, B n -> B (S n)) (n : nat) :
  nat_rect B v0 stp (S n) = stp n (nat_rect B v0 stp n).
Proof. easy. Qed.

Definition fib (n : nat) : R :=
  nth 0 (fib_aux n) 0.

Definition fib_succ : forall n, (1 < n)%nat -> fib n =
  fib (n - 2) + fib (n - 1).
Proof.
intros n ngt1.
unfold fib.
set (m := (n - 2)%nat).
replace n with (S (S m)) by lia.
unfold fib_aux.
rewrite nat_rect_step.
rewrite nat_rect_step.