From df2f50db3703b4f7f88f00ac382c7f3f1efaceb3 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Mon, 23 Feb 2015 11:26:51 +0100
Subject: Fix some typos in comments.

---
 proofs/proof.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/proof.mli')

diff --git a/proofs/proof.mli b/proofs/proof.mli
index 4ae64ae65..2b85ec872 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -134,7 +134,7 @@ exception FullyUnfocused
 exception CannotUnfocusThisWay
 
 (* This is raised when trying to focus on non-existing subgoals. It is
-   handled by an error message but one may need to catched it and
+   handled by an error message but one may need to catch it and
    settle a better error message in some case (suggesting a better
    bullet for example), see proof_global.ml function Bullet.pop and
    Bullet.push. *)
-- 
cgit v1.2.3