Commit f00cbb9c authored by Jonas Kastberg's avatar Jonas Kastberg

Fixed wrong section closing and added exampel to _CoqProject

parent f84033e7
Pipeline #27928 passed with stage
in 20 minutes and 48 seconds
...@@ -17,6 +17,7 @@ theories/examples/sort_br_del.v ...@@ -17,6 +17,7 @@ theories/examples/sort_br_del.v
theories/examples/sort_fg.v theories/examples/sort_fg.v
theories/examples/map.v theories/examples/map.v
theories/examples/map_reduce.v theories/examples/map_reduce.v
theories/examples/subprotocols.v
theories/logrel/model.v theories/logrel/model.v
theories/logrel/kind_tele.v theories/logrel/kind_tele.v
theories/logrel/subtyping.v theories/logrel/subtyping.v
......
...@@ -9,4 +9,4 @@ Section basics. ...@@ -9,4 +9,4 @@ Section basics.
(<! (l1 : loc)> MSG (#l1, #l2') {{ l1 #20 }}; END)%proto. (<! (l1 : loc)> MSG (#l1, #l2') {{ l1 #20 }}; END)%proto.
Proof. iIntros "Hl2'" (l1) "Hl1". iExists l1, l2'. by iFrame "Hl1 Hl2'". Qed. Proof. iIntros "Hl2'" (l1) "Hl1". iExists l1, l2'. by iFrame "Hl1 Hl2'". Qed.
End pair. End basics.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment