This is strange, I did "make vio2vo" before pushing...

Make [ELCtx_Alive] a coercion

See merge request !6

Jacques-Henri Jourdan authored 8 years ago and Jacques-Henri Jourdan committed 8 years ago

This still does not work for parsing, because of a bug in Coq. But at least for printing this is OK, and this is ready for when we will switch to 8.6pl1.

Jacques-Henri Jourdan authored 8 years ago and Jacques-Henri Jourdan committed 8 years ago

I needed to uncurry the [fn] type, so that type inference infers first that the generalized variables are lifetimes, before typechecking the external lifetime contexts.

Jacques-Henri Jourdan authored 8 years ago and Jacques-Henri Jourdan committed 8 years ago

This will make it possible to declare ELCtx_Alive a coercion.

It seems like un-discriminating these hint db does not change
anything.

Make box a definition and prove it contractive

See merge request !5

Fix [solve__typing] by changing the hint on [tctx_extract_hasty_here_eq] into a [Hint Resolve], so that the opaqueness annotations are not ignored.

This also allows us to get rid of ctx_eq

This simplifies the statements of all the toplevel typing theorem, and make them generic on the lifetime contexts, so that they can actually be used.

make the metric on types the expected one; define the old metric as another relation that's used only for constructing the fixpoint

This makes us able to have a smaller mask for ending a lifetime, and hence we get rid of an admit in RwLock.

FIXME : we need to be able to end a lifetime when an invariant is still open.

This requires using a different invariant in the case N ⊥ lftN. Hence, we add the side condition that (N = lftN ∨ N ⊥ lftN). This is not particularly pretty : the alternative would be to have two different kinds of shared borrows.