coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] eauto with destruct

From: Bruno Woltzenlogel Paleo <bruno.wp AT gmail.com>
To: Cedric Auger <sedrikov AT gmail.com>
Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] eauto with destruct
Date: Fri, 24 Jan 2014 17:17:11 +0100

Thanks, Cedric. “firstorder” works.

I also liked “intuition”, but it is still not very intuitive to me why “intuition” and “auto” do not try to destruct H1 in my example (and to destruct certain kinds of hypotheses in general).

[Coq-Club] eauto with destruct, Bruno Woltzenlogel Paleo, 01/24/2014
- Re: [Coq-Club] eauto with destruct, Cedric Auger, 01/24/2014
  - Re: [Coq-Club] eauto with destruct, Bruno Woltzenlogel Paleo, 01/24/2014