The Coq mailing list

[Agnishom Chattopadhyay <agnishom AT cmi.ac.in>]

Hi;

When I try to run the command in line 516 here, I get a strange error:

Function toInc (f : trace indA -> trace indB) `{TraceFunction f} `{Monotone f} (ins : list (trace indA))

{measure length ins} : (list (trace indB)) :=

match (rev ins) with

| [] => [f []]

| (new :: inss) =>

let insofar := (concat (rev inss)) in

(toInc f (rev inss))

++ [proj1_sig (monotonicity_witness insofar (insofar ++ new)

(exist _ new (reflexivity (insofar ++ new))))]

end.

(* Error: Anomaly "File "plugins/funind/gen_principle.ml", line 1526, characters 37-43: Assertion failed."

Please report at http://coq.inria.fr/bugs/.

*)

Is this a known issue with a simple workaround? I tried using `Program Fixpoint` instead, but sadly Program Fixpoint does not generate an equation and creates a term very difficult to work with.