From c8b57f62f5ad12f8926f57fcdbc5bb2ee3c63eff Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 13 Oct 2015 11:40:22 +0200 Subject: Miscellaneous typos, spacing, US spelling in comments or variable names. --- proofs/proof_global.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs/proof_global.mli') diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 028116049..fcb706cc8 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -94,7 +94,7 @@ val start_dependent_proof : val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof (* Intermediate step necessary to delegate the future. - * Both access the current proof state. The formes is supposed to be + * Both access the current proof state. The former is supposed to be * chained with a computation that completed the proof *) type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context -- cgit v1.2.3