From 113376b9923390fccbfb9f6bcec1a645a6e62a19 Mon Sep 17 00:00:00 2001 From: jihgfee <jihgfee@gmail.com> Date: Tue, 30 Jun 2020 15:11:01 +0200 Subject: [PATCH] Renamed mapper example section --- theories/logrel/examples/mapper.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/theories/logrel/examples/mapper.v b/theories/logrel/examples/mapper.v index 9497d30..3183772 100644 --- a/theories/logrel/examples/mapper.v +++ b/theories/logrel/examples/mapper.v @@ -2,7 +2,7 @@ From actris.channel Require Import proofmode proto channel. From actris.logrel Require Import subtyping_rules term_typing_judgment term_typing_rules environments operators subtyping_rules. From iris.proofmode Require Import tactics. -Section with_Σ. +Section mapper_example. Context `{heapG Σ, chanG Σ}. (** Client typing *) @@ -245,5 +245,4 @@ Section with_Σ. { iApply env_split_right=> //; last by iApply env_split_id_r. eauto. } Qed. - -End with_Σ. +End mapper_example. -- GitLab