Type contexts, and their inclusion.
Also, to fix the build: use compatibility layer for ownP. TODO : connect the heap invariant directly.
Showing
- _CoqProject 1 addition, 0 deletions_CoqProject
- opam.pins 1 addition, 1 deletionopam.pins
- theories/lang/adequacy.v 3 additions, 3 deletionstheories/lang/adequacy.v
- theories/lang/derived.v 1 addition, 1 deletiontheories/lang/derived.v
- theories/lang/heap.v 3 additions, 3 deletionstheories/lang/heap.v
- theories/lang/lifting.v 20 additions, 18 deletionstheories/lang/lifting.v
- theories/typing/bool.v 1 addition, 1 deletiontheories/typing/bool.v
- theories/typing/function.v 1 addition, 1 deletiontheories/typing/function.v
- theories/typing/int.v 1 addition, 1 deletiontheories/typing/int.v
- theories/typing/lft_contexts.v 4 additions, 5 deletionstheories/typing/lft_contexts.v
- theories/typing/own.v 1 addition, 1 deletiontheories/typing/own.v
- theories/typing/perm.v 5 additions, 5 deletionstheories/typing/perm.v
- theories/typing/product.v 2 additions, 2 deletionstheories/typing/product.v
- theories/typing/product_split.v 1 addition, 1 deletiontheories/typing/product_split.v
- theories/typing/shr_bor.v 3 additions, 3 deletionstheories/typing/shr_bor.v
- theories/typing/sum.v 2 additions, 2 deletionstheories/typing/sum.v
- theories/typing/type.v 6 additions, 6 deletionstheories/typing/type.v
- theories/typing/type_context.v 115 additions, 0 deletionstheories/typing/type_context.v
- theories/typing/type_incl.v 1 addition, 1 deletiontheories/typing/type_incl.v
- theories/typing/typing.v 1 addition, 1 deletiontheories/typing/typing.v
Loading
Please register or sign in to comment