coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal)

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal)
Date: Wed, 9 Nov 2016 16:43:27 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga02.intel.com
Ironport-phdr: 9a23:5z2NrxA4oeuUv02YTOPbUyQJP3N1i/DPJgcQr6AfoPdwSPT9psbcNUDSrc9gkEXOFd2CrakV0KyO6+u+ACQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9GiTe5b75+Ngm6oRneusQXnIdpN7o8xAbOrnZUYepd2HlmJUiUnxby58ew+IBs/iFNsP8/9MBOTLv3cb0gQbNXEDopPWY15Nb2tRbYVguA+mEcUmQNnRVWBQXO8Qz3UY3wsiv+sep9xTWaMMjrRr06RTiu86FmQwLuhSwaNTA27XvXh9RwgqxFvRyhuxJxzY3aYI6XNfpxYqzSc9wBSGpdR8ZcUzBNDp+gY4cRCecKIOZWr5P6p1sLtRayCxSiBOTxxT9Hmn/2x6o60/w5HQrb2wIgHs4BsHTOo9rrMKceX/2+wa7NzTXCc/xW2S3y55bMchw7uvGMWqx/ccXNyUk1EAPFlk6dqY3jPzOJyOsNt3KX4PZnVeKqkmMqrRx6rDaoxscpkIbJh4QVx0jF9SV/3IY6O9m4RFRmbtG6FpZbqiKUN5NuT88/TWxltzw2xqAItJO0ZiQG1Zoqyh/FZ/CZb4SE+g/vWeefLDtiin9odqiziwi8/EWk0OHwS8q53EtSoiZYk9TBsmoB2wLT58WIUPdx4F2t1SiR2w3S7OxPPFo6mrDBK5E7x749jpoTvlrHHi/xgEj2iaCWeV849uS28ejnY7PmpoOCOI9wkA3xLqMumsmnDeQ5NAgBQXSb9Pyh2LDt8kD1WqhGg/M5n6XDrZzXK8UWqrSnDwNJyooj7gywDzai0NQWh3kHK1dFdQqCj4joJ17OIOr3Aum7g1i2izdrwO7JPrL9ApXXKXjDiKzsfbd7605A1gUzycpT6I5TCrEEOP7zQFP+tMTEDh8lNAy52/roCNJk1o8HRW2PBrKZP7jJvF+T5uMvJvGMa5UPtDb8Lfgl/f/ugmUjlV8TZ6n6lacQPTqzGe0jKEGEa1LthM0AGCEEpEB2GOftkRiJVSNZT3e0RaM1oD8hXtGIF4DGE8qWh7GOwD28BtkeQ2FNClmBFT2gI4CFUPcFZSbUOchsnSAeUqCJSok92BXovwj/nek0ZtHI8zEV4MqwnON+4PfewEk/

Dear Jonathan,

thanks for pointing out the Tactic Notation trick! I give it a try. I would
make sure that I do this in a way so that I can use sed to change to whatever
other mechanism for this is supported in future versions of Coq. This method
might be much faster than the eauto method I use currently, because eauto
repeatedly checks all hints if they solve the goal, which is never the case
in this situation and thus a waste of time.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal), Soegtrop, Michael, 11/09/2016
- Re: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal), Jonathan Leivent, 11/09/2016
  - RE: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal), Soegtrop, Michael, 11/09/2016
    - Re: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal), Jonathan Leivent, 11/09/2016
      - Re: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal), Clément Pit--Claudel, 11/09/2016
        
        Re: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal), Jonathan Leivent, 11/09/2016
        
        Re: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal), Paul A. Steckler, 11/09/2016
      - RE: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal), Soegtrop, Michael, 11/10/2016