Fix compat with Coq 8.15 & fix warnings.
Showing
- theories/examples/folly_queue/refinement.v 11 additions, 11 deletionstheories/examples/folly_queue/refinement.v
- theories/examples/folly_queue/set.v 19 additions, 19 deletionstheories/examples/folly_queue/set.v
- theories/examples/stack/CG_stack.v 1 addition, 1 deletiontheories/examples/stack/CG_stack.v
- theories/examples/stack_helping/offers.v 1 addition, 1 deletiontheories/examples/stack_helping/offers.v
- theories/examples/symbol.v 1 addition, 1 deletiontheories/examples/symbol.v
- theories/examples/various.v 1 addition, 1 deletiontheories/examples/various.v
- theories/experimental/hocap/counter.v 1 addition, 1 deletiontheories/experimental/hocap/counter.v
- theories/lib/lock.v 1 addition, 1 deletiontheories/lib/lock.v
- theories/logic/adequacy.v 1 addition, 1 deletiontheories/logic/adequacy.v
- theories/logic/model.v 1 addition, 1 deletiontheories/logic/model.v
- theories/logic/spec_ra.v 1 addition, 1 deletiontheories/logic/spec_ra.v
- theories/prelude/lang_facts.v 1 addition, 1 deletiontheories/prelude/lang_facts.v
- theories/typing/contextual_refinement.v 2 additions, 2 deletionstheories/typing/contextual_refinement.v
- theories/typing/types.v 5 additions, 5 deletionstheories/typing/types.v
Loading
Please register or sign in to comment