test-suite/bugs/closed/3929.v


1
2
3
4
5
6
7
8
9
10
11
12

Goal True.
evar (T:Type).
pose (Z:=nat).
let Tv:=eval cbv [T] in T in
pose (x:=Tv).
revert x.
refine (_ : let x:=Z in True).
let Zv:=eval cbv [Z] in Z in
let Tv:=eval cbv [T] in T in
constr_eq Zv Tv.
Abort.