Get rid of the `invG` dependency on `lty2`.
Showing
- theories/logic/adequacy.v 3 additions, 3 deletionstheories/logic/adequacy.v
- theories/logic/derived.v 1 addition, 1 deletiontheories/logic/derived.v
- theories/logic/model.v 39 additions, 36 deletionstheories/logic/model.v
- theories/logic/rules.v 1 addition, 1 deletiontheories/logic/rules.v
- theories/tests/proofmode_tests.v 1 addition, 1 deletiontheories/tests/proofmode_tests.v
- theories/typing/fundamental.v 3 additions, 3 deletionstheories/typing/fundamental.v
- theories/typing/interp.v 12 additions, 12 deletionstheories/typing/interp.v
Loading
Please register or sign in to comment