Ssreflect Users Discussion List

[Laurent Théry <>]

On 09/04/2013 03:37 AM, t x wrote:
> 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!

It seems that ssreflect has broken the way "type of" is parsed in Ltac. 
A quick fix is to rename "type of" before loading
ssreflect.

Require Import ZArith String.
Ltac typeOf x := type of x.
Require Import ssreflect eqtype.

Lemma lem:
forall (a b: nat)
(H: {a = b } + {a <> b}), False.
Proof.
move => a b H.
let t := typeOf H in
set (x := t).