Skip to content

Make [ELCtx_Alive] a coercion

Jacques-Henri Jourdan requested to merge jh/alive_coercions into master

I made ELCtx_Alive a coercion.

This has several consequences:

  • lft has to be a definition instead of a notation. In order to make sure that it will not be unfolded, I made it part of the signature of the lifetime logic
  • The parameters of the fn type have to be uncurried, so that the type inference of Coq determines the value of A befor type-checking the external lifetime environment.

What do you think? Is it worth merging as-is or should we use a notation after all?

Merge request reports