Coq8.6 is also compatible with 8.5 - make it the new master

[No text]

coq/ra/examples/circ_buffer.v

+From iris.program_logic Require Export weakestpre.
+From iris.proofmode Require Import tactics.
+
+From ra Require Export notation foundational alloc repeat.
+
+Import uPred.
+
+Section CircBuffer.
+
+  Context (n: positive).
+
+  Local Notation wi := #0.
+  Local Notation ri := #1.
+  Local Notation b := #2.
+
+  Definition newBuffer : base.val :=
+    λ: <>,
+      let: "q" := malloc (#(Z.pos n) + #2) in
+        ["q" + ri]_na <- #0 ;;
+        ["q" + wi]_na <- #0 ;;
+        "q".
+
+  Definition tryProd : base.val :=
+    λ: "q" "x",
+      let: "w" := ["q" + wi]_at in
+      let: "r" := ["q" + ri]_at in
+      let: "w'" := ("w" + #1) `mod` #(Z.pos n) in
+        if: "w'" = "r"
+        then #0
+        else
+          ["q" + b + "w"]_na <- "x" ;;
+          ["q" + wi]_at <- "w'" ;;
+          #1.
+
+  Definition tryCons : base.val :=
+    λ: "q",
+      let: "w" := ["q" + wi]_at in
+      let: "r" := ["q" + ri]_at in
+        if: "w" = "r"
+        then #0
+        else
+          let: "x" := ["q" + b + "r"]_na in
+            ["q" + ri]_at <- ("r" + #1) `mod` #(Z.pos n) ;;
+            "x".
+
+End CircBuffer.
\ No newline at end of file