coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Status of "Hint Cut"

From: Ralf Jung <post AT ralfj.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Status of "Hint Cut"
Date: Wed, 4 Nov 2015 17:11:07 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=post AT ralfj.de; spf=None smtp.mailfrom=post AT ralfj.de; spf=None smtp.helo=postmaster AT zwei.ralfj.de
Ironport-phdr: 9a23:lk8iyBehSe8vFL5ZcXkcJPzelGMj4u6mDksu8pMizoh2WeGdxc64Yh7h7PlgxGXEQZ/co6odzbGG7ua7ASdQuN6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDvvcaLKFURzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IAu3GePEzSqUdBzA7OUg04tfqvF/NV1ih/HwZB18flhQAIRXD41muRpDqrgPgv+5z2m+WMJulHvgPRT2+4vIzG1fTgyAdOmth/Q==

Hi Matthieu,

> this is indeed supported and I'm documenting it right now, thanks
> for the reminder! This works for typeclasses eauto only currently,
> hopefully it will
> be available for the other auto/eauto variants once we merge them.
> Best regards,

Great, thanks for the reply :)

Kind regards,
Ralf

Re: [Coq-Club] Status of "Hint Cut", Ralf Jung, 11/04/2015
- Re: [Coq-Club] Status of "Hint Cut", Matthieu Sozeau, 11/04/2015
  - Re: [Coq-Club] Status of "Hint Cut", Ralf Jung, 11/04/2015
  - Re: [Coq-Club] Status of "Hint Cut", Ralf Jung, 11/04/2015