From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
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)