Ssreflect Users Discussion List

[Maxime Dénès <>]

Hello!

I extracted a small example of a problem which puzzles me. The following 
proof script compiles without any trouble:

Require Import ssreflect ssrfun ssrbool ssrnat seq.

Lemma foo T (s1 s2 : seq (seq T)) : all predT (zip s1 s2).
Proof.
have [//|] := altP (all_nthP ([::],[::])).
by elim: s1 s2=> [[]|x1 s1 IHs []].
Qed.

While if you add zmodp in the Require line, then you get a universe 
inconsistency at Qed. Surprisingly, replacing the "have" tactic by a 
"case" solves the problem. This may be because of the way "have" 
generalizes free variables. In particular, adding a type annotation for 
the empty sequences above is also enough to get rid of the inconsistency.

I'm not sure if this is a bug or not, but it is a bit counter-intuitive. 
I'm running Coq8.4pl1 with ssreflect's trunk.

Maxime.