coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Future

From: Enrico Tassi <enrico.tassi AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Future
Date: Sun, 9 Apr 2017 20:12:01 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=enrico.tassi AT inria.fr; spf=None smtp.mailfrom=gares AT fettunta.org; spf=None smtp.helo=postmaster AT fettunta.org
Ironport-phdr: 9a23:9H5cThBa2pbEXDNdqpISUyQJP3N1i/DPJgcQr6AfoPdwSPryr8bcNUDSrc9gkEXOFd2CrakV16yO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fdbghMizexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJOT43/n/KhMJzgqJUrw6uqAF9zIHae4yVKOZyc7nBcd8GX2dNQMBcXDFBDIOmaIsPCvIMM+ler4nnplsBsRy+DhSyCuz10T9InX721rA93us/FwHGxg0gEM4JsHjOsNX6LrwSUfu0zKTTzDXDaelW2Tbn54TSfBAhu+iBULRtesTS0UkiDwfIg1qKpYD7MT6ZzOUAvmyB4+Z9S+6iiXYrpgJyrzS128shiIrEipgRx13L7yl13Zo5KcC+RUVme9CrCoFQuDufN4ZuQsMtXWVouCEix70Ip5G7YDQKyIkhxx7DcfOLaY+I4gjsVOqJIDd4gmxqeK6nihu2/kWs0PPwW8eu3FtLqidJiMTAum4P2hDL78iIUPp9/kOv2TaV0ADT7/lJIU8umqrBNZEh2aU9lpQNvkTfAi/2hUP2jLOMeUk+/eio8evnbq38ppCAL490lh3+MqM2l8OjBuQ4KxECUHSf+eShz7Lu5lb5QbVPjv0uiKbVqpHaJcIBpq64GQBZyIgj6wzsRwuhhd8fhDwMKE9PUBOBlYngfV/Uc97iCvLqrlK2kTxsj8zPJabgSsHAKGLCm7CnYb9m8E90yQwpzNkZ6YgCWeJJG+76RkKk7I+QNRQ+KQHhm+s=

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