From bcfccc2ab6e47f9bc5820fa412afd3ee974defa1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 29 May 2003 20:52:06 +0000 Subject: [PATCH] New ispell. --- helm/papers/calculemus-2003/hbugs-calculemus-2003.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex index de5172d3b..f0165276c 100644 --- a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex +++ b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex @@ -445,7 +445,7 @@ the \hbugs{} architecture. to share the cache of loaded (and type-checked) theorems. As we will explain in Sect. \ref{tutors}, this feature turns out to be really useful for tactics that rely on a huge but fixed set of lemmas, - as every reflexivite tactic. + as every reflexive tactic. The implementation of a tutor with the described architecture is not that difficult having a language with good threading capabilities (as OCaml has) -- 2.39.2