From f9e4241a7db2f850e47804070a1803056687bd36 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 17 May 2017 18:08:25 +0200
Subject: [PATCH] expand on a comment
---
theories/typing/sum.v | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index e6073d10..585a95e4 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -9,7 +9,8 @@ Section sum.
Context `{typeG Σ}.
(* We define the actual empty type as being the empty sum, so that it is
- convertible to it (and in particular, we can partern-match on it). *)
+ convertible to it---and in particular, we can pattern-match on it
+ (as in, pattern-match in the language of lambda-rust, not in Coq). *)
Program Definition emp0 : type :=
{| ty_size := 1%nat;
ty_own tid vl := False%I;
--
GitLab