Ssreflect Users Discussion List

[Georges Gonthier <>]

   Hello,
Actually, the conflict is with the ssreflect prologue file (ssreflect.v, and 
specifically the ssreflect.SsrSyntax submodule), which makes 'of' into a 
proper keyword, in order to enable the support for datatype declarations 
(e.g., Inductive ordinal n = Ordinal i of i < n). Oddly, of is not recognized 
as a keyword by the Ltac grammar rules. The ssreflect plugin code does some 
obscure backpatching for all known (to us) instances of this in the Ltac 
grammar, but obviously some new (unprotected) rule was added with 8.4 that 
we'll have to cater to.
  In the meantime:
- If you Require but don't Import ssreflect, you'll get the plugin with part 
of the ssreflect functionality. You can define your Ltac functions in this 
context, then call them after doing Import ssreflect.
- you can also substitute a match of a term that gets the type by type 
inference, such as an application of the identity function
   Ltac foo x := match constr: (id x) with @id ?t  _ => idtac t end.

Cheers,
   Georges

-----Original Message-----
From: Erik Martin-Dorel [] 
Sent: 21 November 2012 14:22
To: SSReflect
Subject: Using [match type of] with SSR plug-in

Dear list,

It seems to me that the Ltac invocation [match type of] is unavailable when 
SSReflect has been loaded. Here is a toy example:

================8<================
Coq < Require Import ssreflect.
Coq < Ltac foo x := match type of x with ?t => idtac t end.
Toplevel input, characters 25-27:
> Ltac foo x := match type of x with ?t => idtac t end.
>                          ^^
Syntax error: 'with' expected after [tactic:tactic_expr] (in 
[tactic:tactic_expr]).
================8<================

Would someone know a workaround for using this phrasing when the SSReflect 
plug-in (v1.3pl4 or v1.4) is loaded?

Kind regards,

Erik

--
Érik Martin-Dorel
Post-doctorant, Équipe-projet Marelle
Inria Sophia Antipolis - Méditerranée
http://erik.martin-dorel.org/