Skip to content

GitLab

Closed
Created by Ralf Jung@jungOwner

iNext unfolds things (more than simpl) even when there is no later to strip

See https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/02ef8176f01f8de0563a2f5a8e1444bb9ee01b6d/theories/typing/cont.v#L40: The context goas from

  ​​"HC" : elctx_interp E qE -∗ cctx_interp tid C
  ​"HE" : elctx_interp E qE
  ​"HL" : llctx_interp L1 1
  ​"HT" : tctx_interp tid (T' args)

to

"HC" : elctx_interp E qE -∗ cctx_interp tid C
  ​"HE" : [∗ list] k↦x ∈ E, (λ (_ : nat) (x0 : elctx_elt), elctx_elt_interp x0 qE) k x
  ​"HL" : [∗ list] k↦x ∈ L1, (λ (_ : nat) (x0 : llctx_elt), llctx_elt_interp x0 1) k x
  ​"HT" : [∗ list] k↦x ∈ T' args, (λ (_ : nat) (x0 : tctx_elt), tctx_elt_interp tid x0) k x

but no later is removed. Not even simpl unfolds these definitions.