coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Future

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Future
Date: Mon, 10 Apr 2017 04:30:42 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f196.google.com
Ironport-phdr: 9a23:+vwe+hD8isDUIrYgSLwwUyQJP3N1i/DPJgcQr6AfoPdwSPv7psbcNUDSrc9gkEXOFd2CrakV16yO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fdbghMizexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoIODA5/2PXhMJ+j6xVvQyvqABkzoHOfI2YLuBzcr/Bcd4YQ2dKQ8ZfVzZGAoO5d4YBC/AOPf1fr4n7ulAArAG+BQ63BOP01zRFgX320rch0+QmFwHG0xYgH9UVsHTPqNj4L6gSUeWvw6nJyTXPde9Z2TD46IXRdB0qvPKCXapofMbP1UUiExnJg1aQpID/IT+Zy+UAv3KG4+dkVO+ijXMspRtrrTi13Mgsj5HEhoILxVDA8iV02IM1Kse5SE5/eNKkCYdQuz2DO4t4X88vR2BltDw1yr0Bvp67cywKx4o9yxHDbPyHdpCE4hPlVOmPPTd1nGxpdK67ihqo8kWtyvfwWtep3FtLtCZJj93Bu3EV2xzW8MeHS/99/km72TaI0gDe8uNELlovlarcLZ4hzaQwlp0IsUTYGiL7g0r2jKqMeUUl/uik8fjoYrLjppOELY97lhn+Mrgymsy4Gek3Lg8OX3GC9eug0L3j4Fb2Ta5Rjvw2l6nZqIrVKd4apq6/GQ9V05ws5wyxDze8g5wkmiwMK0sAcxaahaDoPUvPKbb2F6SRmVOpxRVi3PfAdpL7BY7WZizBmazme7ln7FVHmSI8yNle49RfDbRXc6G7YVP4qNGNVkxxCAez2euyUNg=

I get these messages whenever I backtrack across an [abstract] (and I believe I've had a bug open on this for a while, though I may be mis-recalling); are you using [abstract], or any tactics that use [abstract]?

On Sun, Apr 9, 2017, 2:12 PM Enrico Tassi <enrico.tassi AT inria.fr> wrote:

On Sun, Apr 09, 2017 at 04:58:40PM +0200, Laurent Thery wrote:
> Hi,
>
> when running n homemade Ltac tactic, the tactic run smoothly but I get the
> following message
>
> Future: no fix_exn.
>
> You have probably created a Future.computation from a value without passing
> the ~fix_exn argument. You probably want to chain with an already existing
> future instead.
>
> What does this message mean?
> it seems relative to some backtrack I do with first [...|...|...]).
> How can I get rid of it?

This is likely to be a bug. Please open a bug report with enough info
to reproduce it.
Best
--
Enrico Tassi

[Coq-Club] Future, Laurent Thery, 04/09/2017
- Re: [Coq-Club] Future, Enrico Tassi, 04/09/2017
  - Re: [Coq-Club] Future, Jason Gross, 04/10/2017
    - Re: [Coq-Club] Future, Laurent Thery, 04/10/2017