When working in a module with a parameter, C-c C-c keeps trying to pattern match on that parameter... Also, if I explicitly request a case over an implicit parameter, it generates the cases but forgets to pattern match on the parameter. (For instance, when implementing Reflexive properties.)