]> matita.cs.unibo.it Git - helm.git/commitdiff
New ispell.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 29 May 2003 20:52:06 +0000 (20:52 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 29 May 2003 20:52:06 +0000 (20:52 +0000)
helm/papers/calculemus-2003/hbugs-calculemus-2003.tex

index de5172d3b4b81bdf9b53732c8dd534be0a5f13ed..f0165276c9ac7ca7a66dc5adfa0a25b92d53d6b2 100644 (file)
@@ -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)