The Coq mailing list

[Robin Green <greenrd AT greenrd.org>]

I don't understand the explanation of the tactic "apply term in ident"
in the reference manual (v8.2beta4). It seems to me that the
other non-dependent premises of the type of "term" are all generated as
subgoals - but these subgoals are never used for anything! This cannot
be right. Maybe there is a mistake in the manual?

Maybe this sentence:

"If it succeeds, the statement of hypothesis ident
is replaced by the conclusion of the type of ident"

should actually say:

"If it succeeds, the statement of hypothesis ident
is replaced by the conclusion of the type of term"

Is my guess correct?
-- 
Robin