aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/refiner.ml2
1 files changed, 1 insertions, 1 deletions
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)