There was a problem fetching the pipeline mini graph.
Cleaning : remove hints about [product2] from solve_typing (this type is only...
Cleaning : remove hints about [product2] from solve_typing (this type is only for internal use), and removed unnecessary unfold lemmas.
Showing
- theories/typing/borrow.v 2 additions, 4 deletionstheories/typing/borrow.v
- theories/typing/function.v 1 addition, 2 deletionstheories/typing/function.v
- theories/typing/product.v 1 addition, 10 deletionstheories/typing/product.v
- theories/typing/product_split.v 9 additions, 71 deletionstheories/typing/product_split.v
- theories/typing/programs.v 1 addition, 1 deletiontheories/typing/programs.v
- theories/typing/type_context.v 0 additions, 4 deletionstheories/typing/type_context.v
- theories/typing/type_sum.v 2 additions, 2 deletionstheories/typing/type_sum.v
- theories/typing/uninit.v 2 additions, 2 deletionstheories/typing/uninit.v
- theories/typing/uniq_bor.v 3 additions, 4 deletionstheories/typing/uniq_bor.v
Loading
Please register or sign in to comment