Ssreflect Users Discussion List

[t x <>]

Hi,

  Here is my minimal failure case:

https://gist.github.com/anonymous/35b90fd523ace14dffd3

  The code executes fine (with "move =>" replaced with "intros") in plain Coq.

  However, in ssreflect, I get an error

  "Syntax error: 'with' or 'in' ..." on line 10

  How do I rewrite this in ssreflect? (in particular, I want to extract the type of a term).

Thanks!