Ssreflect Users Discussion List

[Jason Gross <>]

  Notation type_of := (fun _ : T => T).

will break syntactic pattern matching.  You need to [eval cbv beta in] it, and this might (or might not) reduce the type in ways you don't want it reduced.

-Jason

On Thu, Jun 19, 2014 at 9:10 AM, Georges Gonthier <> wrote:

  Indeed, this is a known problem, one which I believe is corrected in ssreflect 1.5. It is due to the fact that ‘of’ is a true keyword in ssreflect but not in Coq, and that Coq’s camlp4 parser is sensitive to this. The ssreflect plugin code does hack into the parser to correct this for other uses of ‘of’ in the Ltac grammar, but this feature is a later addition to Ltac.

   IMHO, this should be a Gallina rather than an Ltac feature, and indeed the following

Notation type_of := (fun _ : T => T).

not only works around the problem, but makes this feature available in any Gallina context.

    Georges

 

From: [mailto:] On Behalf Of Jason Gross
Sent: 18 June 2014 14:30
To: ssreflect
Subject: [ssreflect] Ssreflect (1.4) breaks Ltac's type of notation

 

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