The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

> On 22 Sep 2016, at 14:32, Soegtrop, Michael 
> <michael.soegtrop AT intel.com>
>  wrote:
> 
> Dear Coq Users,
>  
> I have the issue that omega sometimes tries to instantiate evars and fails. 
> See the following example:
>  
> The command has indeed failed with message:
> Cannot infer an existential variable of type "Z" in environment:
> x : Z
>  
> Can someone shed some light on this mystery?
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

Require Import Lia.
Require Import ZMicromega.
Require Import VarMap.
Ltac preprocess :=
  zify ; unfold Z.succ in * ; unfold Z.pred in *.

Ltac mylia :=
  preprocess; xlia;
 (
      intros __wit __varmap __ff ;
      change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
      apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl 
true)).


Best,
—
Frédéric