Anomaly "Uncaught exception Not_found."

[ybertot]

Hello, I am using coq-8.9, math-comp-1.9.0, and coq-paramcoq-1.1.1+coq8.9
The following program raises an anomaly:

From mathcomp Require Import all_ssreflect.

Declare ML Module "paramcoq".

Section seq_algorithm.

Definition trigger (P : Type) (s : seq P) (p0 : P) : P :=
  if size s <= 0 then p0 else p0.

End seq_algorithm.

Parametricity seq.
Parametricity bool.
Parametricity nat.
Parametricity trigger.

[proux01]

Thanks for reporting!

I can reproduce and will investigate but cannot promise anything before next week.

In the meantime, replacing all your Parametricity commands by

Parametricity Recursive trigger.
Parametricity trigger.

seems to work better.

There are pending proof obligations, you can handle them with a Parametricity Tactic as in https://github.com/coq-community/paramcoq/blob/master/test-suite/Parametricity.v