Ssreflect Users Discussion List

[<>]

Hello ssreflect users,

I've found that there are a few cases when I need the propositions that can be
inferred from an inductive construction, as provided by Coq's "inversion"
tactic.  What is most unfortunate about this tactics is that it populates the
context, rather than generalizing what it determines.

What is the proper replacement for inversion using the ssreflect methodology?

John