Corrected a few typos

diff --git a/helm/software/components/binaries/matitaprover/SystemDescriptionMatita.html b/helm/software/components/binaries/matitaprover/SystemDescriptionMatita.html
index fbbf4c4bc542f192275be85a669cb8c0536c2041..4ac62f4993c86ff7cda4d415117eae01528d8cfa 100644 (file)
--- a/helm/software/components/binaries/matitaprover/SystemDescriptionMatita.html
+++ b/helm/software/components/binaries/matitaprover/SystemDescriptionMatita.html
@@ -22,14 +22,14 @@ clauses.
 <H3>Implementation</H3>
 
 Matita is written in Objective Caml, a functional language similar to ML
-developed at INRIA. The automatic prover partecipating to the CASC is 
+developed at INRIA. The automatic prover participating to the CASC is 
 a module of 4000 lines, designed with simplicity and ease of integration in mind.
-It uses the fuctor abstraction mechanism of the OCaml language to achieve
+It uses the functor abstraction mechanism of the OCaml language to achieve
 a good degree of reusability (i.e. comparison over terms is an abstract notion,
 that can be instantiated with a reduction aware relation for higher order logics
 like the Calculus of Inductive Constructions on which Matita is based, or a simpler
-alpha equivalence relation for the TPTP first order lnaguage). Matita is based
-on the Curry-Howard Isomorphims, i.e. proofs are lambda-terms of the CIC calculus. 
+alpha equivalence relation for the TPTP first order language). Matita is based
+on the Curry-Howard Isomorphism, i.e. proofs are lambda-terms of the CIC calculus. 
 The automatic prover is thus able to produce a trace suitable for proof term
 reconstruction [HOPR].