From 5e8634d9ad5f87404e59f59888b318ca8367afc1 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Tue, 7 Feb 2012 16:51:44 +0000
Subject: Typo in comments.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14972 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/proof.ml  | 4 ++--
 proofs/proof.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 72730495d7..7487927445 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -68,8 +68,8 @@ module Cond = struct
   (* first attempt at an algebra of condition *)
   (* semantics:
      - [Cannot] means that the condition is not met
-     - [Strict] that the condition is meant
-     - [Loose] that the condition is not quite meant
+     - [Strict] that the condition is met
+     - [Loose] that the condition is not quite met
        but authorises to unfocus provided a condition
        of a previous focus on the stack is (strictly)
        met.
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 12af18f408..7c538cf0e0 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -151,7 +151,7 @@ val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> unit
    a focusing command and a tactic. Transactions are such that if
    any of the atomic action fails, the whole transaction fails.
 
-   During a transaction, the undo visible undo stack is constituted only
+   During a transaction, the visible undo stack is constituted only
    of the actions performed done during the transaction.
 
    [transaction p f] can be called on an [f] using, itself, [transaction p].*)
-- 
cgit v1.2.3