Subject: Ssreflect Users Discussion List
List archive
- 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
- [ssreflect] ? pattern does not work with case, Jason Gross, 06/04/2014
- Re: [ssreflect] ? pattern does not work with case, Enrico Tassi, 06/04/2014
Archive powered by MHonArc 2.6.18.