coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Unfold opposite

From: "Emer Ni Dhomhnaill" <emernd AT hotmail.com>
To: coq-club AT pauillac.inria.fr
Subject: Unfold opposite
Date: Thu, 22 Feb 2001 12:58:02 -0000

Hello,

My name is Emer and I'm implementing a three-valued logic using coq. This is probably a very easy question but does there exist a tactic that can refold definitions... the opposite to the tactic unfold?

Thanks,

Emer
_________________________________________________________________________
Get Your Private, Free E-mail from MSN Hotmail at http://www.hotmail.com.

Unfold opposite, Emer Ni Dhomhnaill
- Re: Unfold opposite, Jean-Christophe Filliatre