Anomaly when deriving subterm relation on polymorphic inductive

mattam82 / Coq-Equations

A function definition package for Coq

http://mattam82.github.io/Coq-Equations

GNU Lesser General Public License v2.1

223 stars 44 forks source link

Anomaly when deriving subterm relation on polymorphic inductive #307

Open kyoDralliam opened 4 years ago

kyoDralliam commented 4 years ago

Polymorphic Inductive t@{u} : unit -> Type@{u} :=
| base : t tt.

Derive Subterm for t.
(* Error: *)
(* Anomaly "File "kernel/univ.ml", line 990, characters 4-10: Assertion failed." *)
(* Please report at http://coq.inria.fr/bugs/. *)

Stumbled upon with Coq 8.10.2, coq-equations 1.2.1+8.10

mattam82 commented 4 years ago

Ah indeed, you need #[universes(polymorphic)] or to set universe polymorphism globally before.