The Coq mailing list

[CJ Bell <siegebell+coq AT gmail.com>]

Other than the let..in expression, I'm not sure if there is another
source of "hidden" terms. For whatever reason, you can write a pattern
that matches against the type, but Coq ignores it:

let g:= constr:(let x:nat:= 0 in True) in
match g with
| let x:bool := _ in _ => idtac "bool"
| let x:nat := _ in _ => idtac "nat"
end.

Coq generates a warning, "Cast not taken into account in constr
pattern," and the output is "bool."


However, there is a workaround -- match the subterm of let..in as a function:

let g:= constr:(let x:nat:= 0 in True) in
match g with
| let x := _ in (@?z x) => match z with
  | (fun _:bool => _) => idtac "bool"
  | (fun _:nat => _) => idtac "nat"
  end
end.

The output of this is "nat," as we would expect. (This works with
context[...] too!)

So now that I think about it, you might just want the following tactic
in order to see all of those "hidden" types:

Ltac let_to_fun :=
  repeat match goal with
  | |- context[?t] => match t with
      | let x := ?y in (@?z x) =>
       change t with (z y)
      end
  end.


-cj