Ssreflect Users Discussion List

[Jason Gross <>]

Thanks!  That's almost what I want.  I want [case], but only if it's casing a bool.  That is, I want a shorter way to do either

hnf; match goal with |- ?T -> _ => try (has_evar T; fail 1); unify T bool end;

  case.

or

hnf; match goal with |- ?T -> _ => unify T bool end;

  case.

(I guess I'd also settle for

match goal with |- bool -> _ => idtac end;

  case.

)

Thanks,

Jason

On Wed, Jun 11, 2014 at 12:22 PM, Assia Mahboubi <> wrote:

Hi Jason,

which action would you like to perform on this example? Something different from
what:

Goal forall b : bool, b = b.

case.

does?

Best,

assia

Le 11/06/2014 13:01, Jason Gross a écrit :

> Hi,
>
> Is there a variant of case/boolP that does not error on the following?
>
> Goal forall b : bool, b = b.
>   case/boolP.
>   (* Toplevel input, characters 0-10:
> Error: _top_assumption_ is used in conclusion. *)
>
> Thanks,
> Jason