Ssreflect Users Discussion List

[Erik Martin-Dorel <>]

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/