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)