The Coq mailing list

[Robin Green <greenrd AT greenrd.org>]

I got a strange error today from trying to do:

applyFwd f_equal

in Coq 8.1pl3 (applyFwd is defined at
http://logical.futurs.inria.fr/cocorico/TacticExts ;)

From chat in #coq on irc.freenode.net I learned that I should instead
do just:

f_equal

which is a special tactic which knows how to apply f_equal properly.

But that's not what this email is about. Apparently, the strange error
message was due to f_equal in "applyFwd f_equal" being interpreted as
meaning the *tactic* called f_equal, not the lemma (f_equal may refer to
either a tactic or a lemma).

I would argue that good computer languages (whether for programming,
proving, or structure data) have the property that if there are
multiple namespaces, either there is never ambiguity or it's always
possible to disambiguate which namespace you mean. Apparently this can
be done using Tactic Notation instead of Ltac, but this still seems
unsatisfactory - after all, what should one do - never use Ltac? Can
something more be done to avoid this kind of confusing error, where a
lemma is mistaken for a tactic?
-- 
Robin