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

[rtetley]

I cannot reproduce on master. Can you check with a more recent version ? There are pre-releases available if need be ! Thanks :-)

[rtetley]

I'll close this, feel free to re-open if it's still an issue !