coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Ralf Jung <jung AT mpi-sws.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Status of "Hint Cut"
Date: Wed, 4 Nov 2015 17:13:17 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
Ironport-phdr: 9a23:FJx7BhIQ+aFfHcLYP9mcpTZWNBhigK39O0sv0rFitYgUKPXxwZ3uMQTl6Ol3ixeRBMOAu68C0LKd4/mocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC0oLsj6viotX6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVWqLjOq88ULZwDTI8Mmlz6te4mwPESF61738SGkcLlBUAVwrY6h7SW4/w9zDlrax6wibMbp6+dqw9RTn3t/QjcxTvkipSbzM=

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