put the existential quantifier inside spec_ctx
Showing
- theories/examples/par.v 8 additions, 8 deletionstheories/examples/par.v
- theories/experimental/helping/helping_stack.v 3 additions, 5 deletionstheories/experimental/helping/helping_stack.v
- theories/logic/adequacy.v 2 additions, 2 deletionstheories/logic/adequacy.v
- theories/logic/compatibility.v 2 additions, 3 deletionstheories/logic/compatibility.v
- theories/logic/model.v 9 additions, 16 deletionstheories/logic/model.v
- theories/logic/proofmode/spec_tactics.v 54 additions, 57 deletionstheories/logic/proofmode/spec_tactics.v
- theories/logic/rules.v 20 additions, 21 deletionstheories/logic/rules.v
- theories/logic/spec_ra.v 3 additions, 3 deletionstheories/logic/spec_ra.v
- theories/logic/spec_rules.v 30 additions, 20 deletionstheories/logic/spec_rules.v
- theories/tests/tp_tests.v 10 additions, 11 deletionstheories/tests/tp_tests.v
- theories/typing/fundamental.v 1 addition, 1 deletiontheories/typing/fundamental.v
Loading
Please register or sign in to comment