Fixing typos - Part 3

3 files changed, 3 insertions, 3 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index c36b0fa337..b022f4596d 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -19,7 +19,7 @@ open Reduction
 open Clenv
 
 (* This function put casts around metavariables whose type could not be
- * infered by the refiner, that is head of applications, predicates and
+ * inferred by the refiner, that is head of applications, predicates and
  * subject of Cases.
  * Does check that the casted type is closed. Anyway, the refiner would
  * fail in this case... *)
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 55dafe521f..b8948a92f3 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 (** The primitive refine tactic used to fill the holes in partial proofs. This
-    is the recommanded way to write tactics when the proof term is easy to
+    is the recommended way to write tactics when the proof term is easy to
     write down. Note that this is not the user-level refine tactic defined
     in Ltac which is actually based on the one below. *)
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index bce227dabb..6476e298e6 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -289,7 +289,7 @@ let tclIFTHENTRYELSEMUST tac1 tac2 gl =
 (* Fails if a tactic did not solve the goal *)
 let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.")
 
-(* Try the first thats solves the current goal *)
+(* Try the first that's solves the current goal *)
 let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl)