From: Claudio Sacerdoti Coen Date: Thu, 29 May 2003 20:52:06 +0000 (+0000) Subject: New ispell. X-Git-Tag: submitted~9 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bcfccc2ab6e47f9bc5820fa412afd3ee974defa1;p=helm.git New ispell. --- 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)