X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineReduction.ml;h=af41d8ee8b42508e0ec802e7b705fdc13edf9a0b;hb=e5efa2e0b70723b431cdc4cffe10b41167145ca4;hp=e43f9221c2d0a503cb46b6a2c145d4fac3438cc9;hpb=73397ea88cd90c04d2a9704e44e5a0bdc5f4675d;p=helm.git

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index e43f9221c..af41d8ee8 100644
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -584,7 +584,7 @@ exception AlreadySimplified;;
 (* Takes a well-typed term and                                               *)
 (*  1) Performs beta-iota-zeta reduction until delta reduction is needed     *)
 (*  2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted  *)
-(*     w.r.t. zero or more variables and if the Fix can be reduced, than it  *)
+(*     w.r.t. zero or more variables and if the Fix can be reductaed, than it  *)
 (*     is reduced, the delta-reduction is succesfull and the whole algorithm *)
 (*     is applied again to the new redex; Step 3) is applied to the result   *)
 (*     of the recursive simplification. Otherwise, if the Fix can not be     *)