From be40007de49140d403bb1dad1af9f4f1e3fe5003 Mon Sep 17 00:00:00 2001
From: JPR
Date: Fri, 24 May 2019 04:42:38 +0200
Subject: Fixing typos

---
 proofs/refiner.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 6476e298e6..799f4a380b 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 that's solves the current goal *)
+(* Try the first that solves the current goal *)
 let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl)
 
 
-- 
cgit v1.2.3