Ssreflect Users Discussion List

[Jason Gross <>]

Is this a known bug?

Require Import Ssreflect.ssreflect.

Ltac foo x := type of x.

(* Toplevel input, characters 19-21:

Syntax error: '.' expected after [vernac:command] (in [vernac_aux]). *)

There's a workaround of doing

Ltac type_of x := type of x.

Require Import Ssreflect.ssreflect.

But it would be nice if ssr made [type of] work.

-Jason