A failure of derive.param1 with template polymorphism in Prop

[herbelin]

Not sure it is very critical, but there seems to be an issue with template polymorphisms ending in Prop:

Inductive K A := C : A -> K A.
Definition L := K True.
From elpi.apps Require Import derive.std.
Elpi derive.param1 K.
Elpi derive.param1 True.
Fail Elpi derive.param1 L.
(* param1: constant does not have the right type: Unable to unify "K True -> Type" with "L -> Prop"
(universe inconsistency: Cannot enforce is_K.u1 <= Prop). *)

Deriving manually however works, so I suspect the generated is_K not to be declared as template polymorphic:

Inductive K A := C : A -> K A.
Definition L := K True.
From elpi.apps Require Import derive.std.
Unset Uniform Inductive Parameters.
Elpi derive.param1 True.
Inductive is_K (A : Type) (PA : A -> Type) : K A -> Type :=
   is_C : forall a : A, PA a -> is_K A PA (C A a).
Definition is_L : L -> Prop := is_K True is_True.