From ad1ab4857c2e2f6f8b1c35650aee3dc15fbce976 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 8 Sep 2020 11:49:15 +0200
Subject: [PATCH] fix a bunch of typos (thanks Tej)

---
 theories/base_logic/bupd_alt.v                  | 2 +-
 theories/base_logic/lib/fancy_updates_from_vs.v | 2 +-
 theories/bi/derived_laws.v                      | 2 +-
 theories/bi/embedding.v                         | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/base_logic/bupd_alt.v b/theories/base_logic/bupd_alt.v
index b40031111..c058493a2 100644
--- a/theories/base_logic/bupd_alt.v
+++ b/theories/base_logic/bupd_alt.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.base_logic Require Export base_logic.
 From iris Require Import options.
 
-(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
+(* The sections add extra BI assumptions, which is only picked up with [Type*]. *)
 Set Default Proof Using "Type*".
 
 (** This file contains an alternative version of basic updates, that is
diff --git a/theories/base_logic/lib/fancy_updates_from_vs.v b/theories/base_logic/lib/fancy_updates_from_vs.v
index 4d3654f68..f1c0ccc10 100644
--- a/theories/base_logic/lib/fancy_updates_from_vs.v
+++ b/theories/base_logic/lib/fancy_updates_from_vs.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
 From iris.base_logic Require Export base_logic.
 From iris Require Import options.
 
-(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
+(* The sections add extra BI assumptions, which is only picked up with [Type*]. *)
 Set Default Proof Using "Type*".
 
 Section fupd.
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index a9710b744..57a016d07 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -2,7 +2,7 @@ From iris.bi Require Export derived_connectives.
 From iris.algebra Require Import monoid.
 From iris Require Import options.
 
-(* The sections add [BiAffine] and the like, which is only picked up with "Type"*. *)
+(* The sections add [BiAffine] and the like, which is only picked up with [Type*]. *)
 Set Default Proof Using "Type*".
 
 (** Naming schema for lemmas about modalities:
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 8a8374852..4a70ddb3b 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -3,7 +3,7 @@ From iris.bi Require Import plainly updates internal_eq.
 From iris.algebra Require Import monoid.
 From iris Require Import options.
 
-(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
+(* The sections add extra BI assumptions, which is only picked up with [Type*]. *)
 Set Default Proof Using "Type*".
 
 Class Embed (A B : Type) := embed : A → B.
-- 
GitLab