The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le 03/11/2021 à 15:09, Chris Dams a écrit :
> Anyone any ideas about this? Am I misusing the module system terribly?

My advice will presumably be unsatisfying, but, as a rule of thumb, 
never put an inductive definition inside a module. On your example, it 
is trivial to move flups outside, since it does not depend on T. But 
even if it was, just parametrize it and move it outside. Something like

Inductive flups {S:Set}: Set := flups1 | flups2 (x:S).

Module Module1 (T: Thing).
   Definition flups := @flups T.S.
End Module1.

Best regards,

Guillaume