Using rocq to compile Alectryon documents

The normal way to compile Coq documents with Alectryon is to use vsrocq. When this is not possible, however, you can use rocq with (much) reduced functionality: Alectryon will be able to parse individual sentences and refer to them, but not to compute goals and messages. To compile with coqc, pass --coq-driver={sertop_noexec|coqc_time} to Alectryon:

alectryon --coq-driver=vsrocq coq_drivers.v -o coq_drivers.html
  # Coq+reST → HTML; produces ‘coq_drivers.html’

alectryon --coq-driver=coqc_time coq_drivers.v -o coq_drivers.coqc.html
  # Coq+reST → HTML; produces ‘coq_drivers.coqc.html’

Lemma fold_left_app : forall {A B} (f: A -> B -> A) (l l': list B) a,
    fold_left f (l ++ l') a = fold_left f l' (fold_left f l a).
forall (A B : Type) (f : A -> B -> A) 
  (l l' : list B) (a : A),
fold_left f (l ++ l') a =
fold_left f l' (fold_left f l a)
Proof.1
forall (A B : Type) (f : A -> B -> A) 
  (l l' : list B) (a : A),
fold_left f (l ++ l') a =
fold_left f l' (fold_left f l a)
  induction l; simpl; auto.
Qed.

Goal forall {A B} (f: A -> B -> B) (l: list A) b,
    fold_right f b l = fold_left (fun acc b => f b acc) (rev l) b.2
forall (A B : Type) (f : A -> B -> B) 
  (l : list A) (b : B),
fold_right f b l =
fold_left (fun (acc : B) (b0 : A) => f b0 acc) 
  (rev l) b
Proof.
forall (A B : Type) (f : A -> B -> B) 
  (l : list A) (b : B),
fold_right f b l =
fold_left (fun (acc : B) (b0 : A) => f b0 acc) 
  (rev l) b
  intros.
A, B: Type
f: A -> B -> B
l: list A
b: B
fold_right f b l =
fold_left (fun (acc : B) (b0 : A) => f b0 acc) 
  (rev l) b
  induction l; simpl; intros.
A, B: Type
f: A -> B -> B
b: B
b = b
A, B: Type
f: A -> B -> B
a: A
l: list A
b: B
IHl: fold_right f b l =
fold_left (fun (acc : B) (b : A) => f b acc) (rev l) b
f a (fold_right f b l) =
fold_left (fun (acc : B) (b0 : A) => f b0 acc)
  (rev l ++ a :: nil) b
  -
A, B: Type
f: A -> B -> B
b: B
b = b reflexivity.
  -
A, B: Type
f: A -> B -> B
a: A
l: list A
b: B
IHl: fold_right f b l =
fold_left (fun (acc : B) (b : A) => f b acc) (rev l) b
f a (fold_right f b l) =
fold_left (fun (acc : B) (b0 : A) => f b0 acc)
  (rev l ++ a :: nil) b rewrite IHl, fold_left_app; simpl; auto.
Qed.

Check nat.
nat
     : Set

Limited reference functionality is still available: 1, 2, Goal forall {A B} (f: A -> B -> B) (l: list A) b, fold_right f b l = fold_left (fun acc b => f b acc) (rev l) b..