Ssreflect Users Discussion List

[Erik Martin-Dorel <>]

Hello,

Thank you very much for your detailed answer and the nice workaround.

Kind regards,

Erik

----- Mail original -----
> De: "Georges Gonthier" <>
> À: "Erik Martin-Dorel" <>, "SSReflect" 
> <>
> Envoyé: Mercredi 21 Novembre 2012 21:18:51
> Objet: RE: Using [match type of] with SSR plug-in
> 
> 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/