From 7c06dc3541eb8d3652c7b9092ddbb75167e735c4 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 22 Apr 2018 14:07:01 -0400 Subject: [PATCH] Proofreading DeepAndShallowEmbeddings --- DeepAndShallowEmbeddings.v | 8 ++++---- DeepAndShallowEmbeddings_template.v | 6 +++--- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/DeepAndShallowEmbeddings.v b/DeepAndShallowEmbeddings.v index 7d4fbd6..71ae07f 100644 --- a/DeepAndShallowEmbeddings.v +++ b/DeepAndShallowEmbeddings.v @@ -22,9 +22,9 @@ Example h0 : heap := $0 $+ (0, 2) $+ (1, 1) $+ (2, 8) $+ (3, 6). Hint Rewrite max_l max_r using linear_arithmetic. Ltac simp := repeat (simplify; subst; propositional; - try match goal with - | [ H : ex _ |- _ ] => invert H - end); try linear_arithmetic. + try match goal with + | [ H : ex _ |- _ ] => invert H + end); try linear_arithmetic. (** * Basic concepts of shallow, deep, and mixed embeddings *) @@ -510,7 +510,7 @@ End Deep. Module Deeper. (* All programs in the last embedding must terminate, but let's add loops with * the potential to run forever, which takes us beyond what is representable - * in the shallow embedding, since Gallina enforces terminating of all + * in the shallow embedding, since Gallina enforces termination for all * programs. *) (* We use this type to represent the outcome of a single loop iteration. diff --git a/DeepAndShallowEmbeddings_template.v b/DeepAndShallowEmbeddings_template.v index df58f71..5365fad 100644 --- a/DeepAndShallowEmbeddings_template.v +++ b/DeepAndShallowEmbeddings_template.v @@ -17,9 +17,9 @@ Example h0 : heap := $0 $+ (0, 2) $+ (1, 1) $+ (2, 8) $+ (3, 6). Hint Rewrite max_l max_r using linear_arithmetic. Ltac simp := repeat (simplify; subst; propositional; - try match goal with - | [ H : ex _ |- _ ] => invert H - end); try linear_arithmetic. + try match goal with + | [ H : ex _ |- _ ] => invert H + end); try linear_arithmetic. (** * Basic concepts of shallow, deep, and mixed embeddings *)