]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/papers/calculemus-2003/hbugs-calculemus-2003.tex
New ispell.
[helm.git] / 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)