The Coq mailing list

[Jan-Oliver Kaiser <janno AT mpi-sws.org>]

Hello,

I am trying to find occurrences of an instantiated existential variable 
in a bigger term. I have yet to find a way to make this work. I have, 
however, identified a rather peculiar minimal failing example of 
interaction between evars and match context:

(* Some notation to hide a the overhead associated with evars *)
Tactic Notation "exvar" constr(type) tactic(cnt) :=
  let name := fresh in
  evar (name : type);
  let var := (eval unfold name in name) in
  clear name;
  cnt var.

Goal True.
  exvar Type (fun t => unify t nat; match nat with context f [nat] => 
idtac "yay" end).
  Fail exvar Type (fun t => unify t nat; match nat with context f [t] 
=> idtac "yay" end).
Abort.

The first call to exvar is just a sanity check to see if the evar 
machinery works and the context pattern work as intended. The second 
call is what really baffles me. t is successfully unified with nat - but 
it cannot be found in the term nat. What is going on here?

Thanks,
Jan-Oliver