The Coq mailing list

[Nadeem Abdul Hamid <nadeem AT acm.org>]

A few questions about the Coq tactic language:

(1) Say I want to write a simple tactic like the following:

Match Context With [V:?/\? |- ?] -> Elim V; Clear V; Intros V' V.

where I really want V' to be a "fresh" name for the given context, not 
literally "V'"- as is this tactic might fail if I already have a 
hypothesis in the context labeled "V'". Is there a way to do this 
introduction of fresh variables?

(2) In Chapter 10 of the Coq reference manual, figure 10.1, at the 
bottom of the last production in the figure (arg), there is a " 'term" 
case. What is this apostrophe used for? I don't see it described anywhere.

Thanks,

--- nadeem