coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Applying the Quote tactic to terms

From: James Power <James.Power AT May.ie>
To: coq-club AT pauillac.inria.fr
Subject: Applying the Quote tactic to terms
Date: Fri, 13 Aug 1999 15:24:11 +0100
Organization: Dept. of Computer Science, NUI Maynooth

Hi,

I've been playing with the Quote tactic a little, and I was wondering if
there was some way of applying it to just a term in the goal, rather
than the whole goal?

I'm guessing that one way would be to write a more flexible interface to
the quote_terms function in $COQTOP/tactics/contrib/polynom/quote.ml,
but I was wondering if there was a more high-level way of doing this?

James Power,
Dept. of Computer Science, National University of Ireland,
Maynooth, Co. Kildare, Ireland.
Phone: +353-1-7083447 http://www.cs.may.ie/~jpower/

Applying the Quote tactic to terms, James Power