Ssreflect Users Discussion List

[Enrico Tassi <>]

On Thu, Aug 14, 2014 at 01:48:18PM +0100, Jason Gross wrote:
> 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. *)

On trunk with ssr 1.5 I get:

  Error:
  In environment
  nPH : {ab : Set * Set | ab = ab}
  The term "nPH" has type "{ab : Set * Set | ab = ab}" while it is
  expected to have type
   "{x : ?6 & ?7 x}".

On Coq 8.4 with ssr 1.5 I get:

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

Hence, it is not a bug in Ssr, and has been fixed in Coq already.

Best,
-- 
Enrico Tassi