Report upstream: Anomaly "Uncaught exception Not_found."

[skeuchel]

The following snippet

From Katamaran Require Import Context.

Import ctx ctx.notations.

Inductive dom (w : Ctx nat) : Prop :=
  dom_intro : (forall α (αIn : α ∈ w), dom (w - α)) -> dom w.

Definition dom_inv w (d : dom w) :
  forall α (αIn : α ∈ w), dom (w - α) := let (f) := d in f.

Fixpoint dom_step w α (d : dom w) {struct d} : dom (w ▻ α) :=
  @dom_intro _
    (fun β βIn =>
       match view βIn in SnocView βIn return dom (remove βIn) with
       | isZero   => d
       | isSucc i => @dom_step _ _ (@dom_inv _ d _ i)
       end).

crashes with

Error: <in exception printer>: Anomaly "Uncaught exception Not_found."
Please report at http://coq.inria.fr/bugs/.
<original exception>: Uncaught exception Pretype_errors.PretypeError(_, _, _).

Adding the explicit type signature (βIn : β ∈ ctx.snoc w α) inside of dom_step fixes this.

[skeuchel]

Also fixed by the bidirectionality hint Arguments dom_intro [w] & _.