Guard failure at Qed time crashes the server

[YaZko]

It seems like the Guarded command is properly handled. Trying to Defined an ill-guarded interactive cofix is properly rejected, with the right error message. But for some reason trying to Qed an ill-guarded interactive cofix seems to crash the whole server.

See the following self-contained example, on 2.1.0+coq8.19:

Set Primitive Projections.

CoInductive t : Set := mk { pred : option t }.

CoInductive equal : t -> t -> Prop  :=
| equal_zero : equal (mk None) (mk None)
| equal_succ x y : equal x y -> equal (mk (Some x)) (mk (Some y)).

Lemma equal_refl : forall x, equal x x.
Proof.
	cofix cih.
	intros x.
	destruct (pred x) as [x' | ] eqn:eq; auto.
	(* correct error reported *)
	Guarded.
	(* correct error reported *)
	Defined.
	(* But switching to Qed. crashes everything instead of reporting the error *)

It crashes with the attached trace on my machine.
trace.json

Best,
Yannick