Ssreflect Users Discussion List

[Georges Gonthier <>]

  Hi Jason,

this should work, or at least you shouldn’t be getting this error message.

Ssreflect doesn’t do anything to “fresh”, so I suspect the problem might be taking into account the local Ltac bindings in the equation name argument of ‘case’. Looking at the code, it seems that the interp_ipat function isn’t called for the equation name/pattern, probably as an unwanted side effect of some refactoring (the function is now only defined on lists of patterns, and probably used to be defined on single patterns, and automagically called via the TYPED AS clause of TACTIC EXTEND). Hopefully Enrico should be able to patch this easily enough, by using an ssripat == ssripatrep list instead of an  ssripatrep option for ssreqid.

  In the meantime your only option will be to manually emulate the case E: <open term> => <pattern> idiom when E is Ltac-bound, as follows:

   let x := fresh “top” in set x := <open term>; case: @x {-2}x (refl_equal x) => <pattern> E.

In your particular example <open term> is just the single variable H, which can be repeated harmlessly, so you can dispense with the x and just use

   case: {-2}H (refl_equal H) => [?|] E //.

As for your last question, you’re welcome to talk to me, but the best forum is the ssreflect mailing list (in cc: ).

   Cheers,

Georges

  

 

From: Jason Gross [mailto:]
Sent: 03 June 2014 15:59
To: Georges Gonthier
Subject: Question about ssreflect

 

Hi,

Is [fresh] supposed to work with ssreflect (version 1.4)?  The code

 

Goal forall x y : option Type, x = y.
intros.
do 2 lazymatch goal with
         | [ H : option _ |- _ ] => let E := fresh "K" in case E: H => [?|] => //
       end.

 

fails with

Toplevel input, characters 83-100:
Error: E is already used.

 

By the way, should I be asking questions like this to you in person, or IMing you with Lync, or emailing you, or emailing coq-club, or something else?

 

Thanks,

Jason