Bump Iris and fix compilation with Coq master.
Due to changes to Coq's import mechanism, I now made sure that Autusubst is imported first. This caused various things to break, which I patched up.
Showing
- opam 1 addition, 1 deletionopam
- theories/examples/par.v 5 additions, 5 deletionstheories/examples/par.v
- theories/examples/symbol.v 2 additions, 2 deletionstheories/examples/symbol.v
- theories/examples/various.v 26 additions, 26 deletionstheories/examples/various.v
- theories/logic/adequacy.v 1 addition, 1 deletiontheories/logic/adequacy.v
- theories/logic/spec_ra.v 1 addition, 1 deletiontheories/logic/spec_ra.v
- theories/prelude/asubst.v 1 addition, 4 deletionstheories/prelude/asubst.v
- theories/typing/contextual_refinement.v 2 additions, 3 deletionstheories/typing/contextual_refinement.v
- theories/typing/interp.v 1 addition, 1 deletiontheories/typing/interp.v
- theories/typing/soundness.v 1 addition, 1 deletiontheories/typing/soundness.v
- theories/typing/types.v 2 additions, 2 deletionstheories/typing/types.v
Loading
Please register or sign in to comment