The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 11/02/2012 11:16 AM, Charles D wrote:
> I'm using Coq 8.3pl1, and I'd like to use "inversion_clear ... as" to name my 
> hypotheses in an "intelligent" manner, that is, avoiding to fill in names for 
> variables/hypotheses that will be cleared by the tactic.
>
> For instance, in the following code, I'd want my introduction pattern "[a1 b1 ORD|]" to 
> correspond to the 2 variables and 1 hypothesis that remain in the left subgoal, but instead I 
> have "H4" as the name of the generated hypothesis,and ORD is nowhere to be seen. 
> Indeed, ORD has been used to name a hypothesis, but it has been eliminated before the user could 
> actually see the result of the tactic.
>    

Let me just add one plug for an alternative approach: always take the 
default names, and never write names manually.  Instead, use Ltac 
pattern-matching to find them.  More detail on the approach in CPDT:
    http://adam.chlipala.net/cpdt/