Ssreflect Users Discussion List

[Jason Gross <>]

Hi,

The [have] tactic doesn't seem to like [let ... := ... in ...] in ssr 1.4:

Require Import Ssreflect.ssreflect.

Goal True.

  have H' := (fun nPH : { ab : Set * Set | ab = ab }

              => let H := projT2 nPH in 

                 let n := fst (projT1 nPH) in

                 let P := snd (projT1 nPH) in

                 existT (fun ab : Set * Set => ab = ab) _ (_ H)). (* Toplevel input, characters 0-357:

Anomaly: Uncaught exception Invalid_argument("index out of bounds").

Please report. *)

-Jason