Ssreflect Users Discussion List

[Aleksandar Nanevski <>]

Hi.

I just installed Coq-8.2pl1 and the new ssreflect, and have been playing 
with it, when I noticed an unexpected behavior of rewrite in the 
presence of existential variables. In the following script:

Require Import ssreflect ssrnat.

Goal forall x y, exists z, x + y + z = x + (y + z).
move => x y; econstructor.
rewrite addnA.

the last rewrite selects the evar corresponding to z, and modifies it 
into a sum of two fresh evars. That is, I get the subgoal

 x : nat
 y : nat
 ============================
  x + y + ?39 + ?40 = x + (y + (?39 + ?40))

In the previous versions of ssreflect, I would simply get that no 
rewrite is possible, which seems to me like the correct behavior.

After some testing, I realized that Coq proper, with no ssr, behaves in 
this erratic way in both v8.2 and v8.1 (at least since pl5). Can anybody 
please explain the reasons for these features/bugs in Coq, and why 
ssreflect decided to follow suit?

Btw, this used to work correctly in v8.2 with a pre-release version of 
ssreflect-1.2, from about a month ago.
But now it is causing me a lot of erratic Ltac behavior (which, I guess, 
should not be surprising).

Thanks,
-Aleks