Assertion failed with funelim

[Tuplanolla]

Version

Coq 8.13.2

Operating system

Red Hat Enterprise Linux Workstation 7.4

Description of the problem

The following program causes an anomaly.

From Coq Require Import Lia NArith.NArith Program.Basics ssr.ssreflect.
From Equations Require Export Equations.

Obligation Tactic := idtac.

Section Context.

Import N.

Local Open Scope N_scope.

Context (f : N -> N) (mono : forall (a b : N) (l : a < b), f a < f b).

Equations f_bogus (n : N) : positive :=
  f_bogus n :=
    let m := f (succ n) - f n in
    match m with
    | N0 => _
    | Npos p => p
    end.
Next Obligation. intros n m. apply xH. Qed.

Equations f_inspect (n : N) : positive :=
  f_inspect n :=
    let m := f (succ n) - f n in
    match exist _ m (eq_refl m) with
    | exist _ N0 e => @const _ (m = N0) _ e
    | exist _ (Npos p) e => @const _ (m = Npos p) p e
    end.
Next Obligation. intros n m _ _ e. pose proof mono n (succ n) as l. lia. Qed.

Lemma eq_f (n : N) : f_bogus n = f_inspect n.
Proof.
  funelim (f_bogus _). funelim (f_inspect _).
  set (m := f (succ n) - f n). generalize (eq_refl m). case : {2 3 4} m.
  - intros e. subst m. pose proof mono n (succ n) as l. lia.
  - intros p e. reflexivity. Restart.
  funelim f_bogus.

End Context.

Anomaly "File "src/sigma_types.ml", line 118, characters 10-16: Assertion failed."
Please report at http://coq.inria.fr/bugs/.

Notes

This is probably a duplicate of #194,
although the reproduction of this bug does not involve
implicit arguments or Greek letters.

[mattam82]

Indeed it was the same problem funelim should be called with a fully applied term. I turned this into an error for now.