Skip to Content.
Sympa Menu

coq-club - [Coq-Club] compute term

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] compute term


chronological Thread 

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.




Archive powered by MhonArc 2.6.16.

Top of Page