summaryrefslogtreecommitdiffstats
path: root/site
diff options
context:
space:
mode:
Diffstat (limited to 'site')
-rw-r--r--site/posts/StronglySpecifiedFunctions.org4
-rw-r--r--site/posts/StronglySpecifiedFunctionsProgram.v2
-rw-r--r--site/posts/StronglySpecifiedFunctionsRefine.v2
3 files changed, 4 insertions, 4 deletions
diff --git a/site/posts/StronglySpecifiedFunctions.org b/site/posts/StronglySpecifiedFunctions.org
index 9bd488d..805b944 100644
--- a/site/posts/StronglySpecifiedFunctions.org
+++ b/site/posts/StronglySpecifiedFunctions.org
@@ -12,6 +12,6 @@ results are correct too. However, implementing dependently-typed functions can
be challenging. In this series, we explore several approaches available to Coq
developers.
-- [[./StronglySpecifiedFunctionsRefine.html][Using the ~refine~ Tactics]] ::
+- [[./StronglySpecifiedFunctionsRefine.html][Implementing Strongly-Specified Functions with the ~refine~ Tactic]] ::
-- [[./StronglySpecifiedFunctionsProgram.html][Using the ~Program~ Framework]] ::
+- [[./StronglySpecifiedFunctionsProgram.html][Implementing Strongly-Specified Functions with the ~Program~ Framework]] ::
diff --git a/site/posts/StronglySpecifiedFunctionsProgram.v b/site/posts/StronglySpecifiedFunctionsProgram.v
index 8ffb70c..1b4ab5f 100644
--- a/site/posts/StronglySpecifiedFunctionsProgram.v
+++ b/site/posts/StronglySpecifiedFunctionsProgram.v
@@ -1,4 +1,4 @@
-(** * Strongly-Specified Functions in Coq, part 2: the <<Program>> Framework
+(** * Implementing Strongly-Specified Functions with the <<Program>> Framework
This is the second article (initially published on #<span
id="original-created-at">January 01, 2017</span>#) of a series of two on how
diff --git a/site/posts/StronglySpecifiedFunctionsRefine.v b/site/posts/StronglySpecifiedFunctionsRefine.v
index d9bb3aa..1d4ec2e 100644
--- a/site/posts/StronglySpecifiedFunctionsRefine.v
+++ b/site/posts/StronglySpecifiedFunctionsRefine.v
@@ -1,4 +1,4 @@
-(** * Strongly-Specified Functions in Coq, part 1: using the <<refine>> Tactic *)
+(** * Implementing Strongly-Specified Functions with the <<refine>> Tactic *)
(** This is the first article (initially published on #<span
class="original-created-at">January 11, 2015</span>#) of a series of two on