From db0f87d6544a09cfb9c3b832b397a0a58dfadb25 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Mon, 24 Apr 2017 09:28:48 -0400 Subject: [PATCH] DeepAndShallowEmbeddings: comment typo fix --- DeepAndShallowEmbeddings.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DeepAndShallowEmbeddings.v b/DeepAndShallowEmbeddings.v index 660d2bf..7d4fbd6 100644 --- a/DeepAndShallowEmbeddings.v +++ b/DeepAndShallowEmbeddings.v @@ -543,7 +543,7 @@ Module Deeper. done. (* Next, we write a single-stepping interpreter for this language. We can - * know longer write a straightforward big-stepping interpeter, as programs of + * no longer write a straightforward big-stepping interpeter, as programs of * the object language can diverge, while Gallina enforces termination. *) Inductive stepResult (result : Set) :=