coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Problem with "once" tactical and "constructor"

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Problem with "once" tactical and "constructor"
Date: Sun, 01 Feb 2015 15:33:29 -0500

On 02/01/2015 03:21 PM, Jason Gross wrote:

It would seem so, given that

Hint Extern 0 (bar ?f) => destruct f.
Hint Extern 0 => constructor.
Hint Extern 0 => reflexivity.

is not sufficient to make [eauto] solve the goal.

But, "all:solve [auto]" does solve it with those hints. But, "all:solve [eauto]" doesn't. That's probably a bug.

-- Jonathan

Re: [Coq-Club] Problem with "once" tactical and "constructor", Jonathan Leivent, 02/01/2015
- Re: [Coq-Club] Problem with "once" tactical and "constructor", Jason Gross, 02/01/2015
  - Re: [Coq-Club] Problem with "once" tactical and "constructor", Jonathan Leivent, 02/01/2015
    - Re: [Coq-Club] Problem with "once" tactical and "constructor", Jonathan Leivent, 02/01/2015
      - Re: [Coq-Club] Problem with "once" tactical and "constructor", Arnaud Spiwack, 02/02/2015