Skip to Content.
Sympa Menu

ssreflect - Re: [ssreflect] ? pattern does not work with case

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] ? pattern does not work with case


Chronological Thread 
  • From: Enrico Tassi <>
  • To:
  • Subject: Re: [ssreflect] ? pattern does not work with case
  • Date: Wed, 4 Jun 2014 14:28:20 +0200

On Wed, Jun 04, 2014 at 12:11:32PM +0100, Jason Gross wrote:
> In the code
>
> Require Import ssreflect.
> Goal forall x y : bool, x = y.
> intros.
> case ?: x => [|].
>
> The [case] does not introduce an equation hypothesis. If I replace the "?"
> with, say, "H", then I get an equation hypothesis. Is this expected
> behavior?

No time to check the code, but it is probably another manifestation of
the bug you signalled yesterday. If the "intro pattern" on the left of
":" was processed by the standard routines, then you should get an
equation that uses an inaccessible name as in "move=> ?".

I suppose you use 8.4 (given that trunk is broken badly).
Remember to ping me on friday at the Coq GT, I should be easy to fix.

Ciao
--
Enrico Tassi



Archive powered by MHonArc 2.6.18.

Top of Page