coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Casteran <pierre.casteran AT labri.fr>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] compute term
- Date: Wed, 16 Mar 2005 11:50:21 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hello,
Is there a simple way (perhaps with Ltac) to perform a conversion tactic
like compute on some (occurrences of) a term in a goal?
It works with simpl but sometimes I need compute or any conversion tactic.
Pierre
--
Pierre Casteran
http://www.labri.fr/Perso/~casteran/
(+33) 540006931
----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.
- [Coq-Club] compute term, Pierre Casteran
Archive powered by MhonArc 2.6.16.