Merge remote-tracking branch 'origin/master' into ci/gen_proofmode

.gitlab-ci.yml

@@ -20,6 +20,8 @@ variables:
   - 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \((real|user): [0-9]" | tee build-time.txt'
   # maybe validate
   - 'if [[ -n "$VALIDATE" ]]; then make validate; fi'
+  # maybe create opam package
+  - 'if [[ -n "$OPAM_PKG" && "$CI_COMMIT_REF_NAME" == master ]]; then curl --fail -X POST -F "token=$OPAM_UPDATE_SECRET" -F "ref=master" -F "variables[REPO]=$CI_PROJECT_URL.git" -F "variables[REF]=$CI_COMMIT_REF_NAME" -F "variables[SHA]=$CI_COMMIT_SHA" -F "variables[NAME]=$OPAM_PKG" https://gitlab.mpi-sws.org/api/v4/projects/581/trigger/pipeline; fi'
   cache:
     key: "$CI_JOB_NAME"
     paths:

README.md

@@ -6,7 +6,7 @@ This is the Coq development accompanying lambda-Rust.
 
 This version is known to compile with:
 
- - Coq 8.6.1 / 8.7.1
+ - Coq 8.6.1 / 8.7.2
  - Ssreflect 1.6.4
  - A development version of [Iris](https://gitlab.mpi-sws.org/FP/iris-coq/)
 

theories/lang/lib/new_delete.v

@@ -34,7 +34,8 @@ Section specs.
     {{{ RET #☠; True }}}.
   Proof.
     iIntros (? Φ) "(H↦ & [H†|%]) HΦ";
-      wp_lam; wp_op; case_bool_decide; try lia; wp_if; try wp_free; by iApply "HΦ".
+      wp_lam; wp_op; case_bool_decide; try lia;
+      wp_if; try wp_free; by iApply "HΦ".
   Qed.
 End specs.