Skip to Content.
Sympa Menu

coq-club - DInd

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

DInd


chronological Thread 
  • From: Healfdene Goguen <hhg AT dcs.ed.ac.uk>
  • To: coqdev AT margaux.inria.fr
  • Subject: DInd
  • Date: Mon, 09 Feb 1998 14:54:32 +0000

Hello,

Has the "DInd" tactic disappeared in Coq V6.2?  Is there a suggested
replacement?  (Perhaps "Induction; Unify"?)

I used this tactic in many of my proof scripts.

Yours,
Healf GOGUEN





Archive powered by MhonArc 2.6.16.

Top of Page