The Coq mailing list

[Andrew McCreight <andrew.mccreight AT yale.edu>]

On Thu, 3 Oct 2002, Nadeem Abdul Hamid wrote:
> (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.

As far as I can tell, the apostrophe basically just lifts a CIC term to
the level of the tactic language.  Without it, you can't, for instance, 
apply anything more complex terms to a function tactic.

Foo (plus O O)

is not a syntactically valid tactic, while

Foo '(plus O O)

is.


-Andrew