coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] intros []

From: Théo Zimmermann <theo.zimmermann AT ens.fr>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] intros []
Date: Thu, 21 Apr 2016 15:10:17 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmermann AT ens.fr; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f46.google.com
Ironport-phdr: 9a23:+5LWQx/Dn2AvW/9uRHKM819IXTAuvvDOBiVQ1KB91ekcTK2v8tzYMVDF4r011RmSDdWdtaIP27GempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lSsiM34/njKibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwu3cYh/V0vcVHSODxe7kyZb1eFjUvdW4vroW/vh7aCACL+3E0U2MMkxMODRKTvz/gWZKkjit7sd1P2SyfMNfzRLYyEWC+76psDg3pjSIKLTsw9mf/h8pryqxB9kHy7ydjypLZNdnGfMF1ebnQKIsX

Hello,

For a goal of the form A /\ B -> C, using intros [] yields the goal A -> B -> C (and does not add anything to the context). I would have rather expected that A and B be added to the context (this can be achieved with intros [] **).

Is this a wanted behavior? If yes, is it documented somewhere? (I looked but did not find any mention of this pattern in the section of the manual devoted to intros intro_pattern_list).

Thanks,

Théo

[Coq-Club] intros [], Théo Zimmermann, 04/21/2016
- Re: [Coq-Club] intros [], Guillaume Melquiond, 04/21/2016
  - Re: [Coq-Club] intros [], Dominique Larchey-Wendling, 04/21/2016
  - Re: [Coq-Club] intros [], Gabriel Scherer, 04/21/2016
    - Re: [Coq-Club] intros [], Hugo Herbelin, 04/21/2016