coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Why does omega try to instantiate evars (sometimes)

From: Laurent Thery <Laurent.Thery AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Why does omega try to instantiate evars (sometimes)
Date: Thu, 22 Sep 2016 15:55:12 +0200

On 09/22/2016 03:41 PM, Frédéric Besson wrote:

I cannot. Yet, since this summer, lia does not fail on your example.
In 8.5, this is still possible at the cost of rewriting a bit the top-level
lia tactic i.e

At least lia is behaving identically inside and outside an ltac which is not the case for omega.

will this patch be included in the next version of lia?

--
Laurent

[Coq-Club] Why does omega try to instantiate evars (sometimes), Soegtrop, Michael, 09/22/2016
- Re: [Coq-Club] Why does omega try to instantiate evars (sometimes), Frédéric Besson, 09/22/2016
  - Re: [Coq-Club] Why does omega try to instantiate evars (sometimes), Laurent Thery, 09/22/2016
  - RE: [Coq-Club] Why does omega try to instantiate evars (sometimes), Soegtrop, Michael, 09/22/2016
    - Re: [Coq-Club] Why does omega try to instantiate evars (sometimes), Frédéric Besson, 09/22/2016
      - RE: [Coq-Club] Why does omega try to instantiate evars (sometimes), Soegtrop, Michael, 09/22/2016
- Re: [Coq-Club] Why does omega try to instantiate evars (sometimes), Jonathan Leivent, 09/22/2016