From d52f1a1f765a91ba285d9623da7e8afecc0af1b5 Mon Sep 17 00:00:00 2001 From: Thibault Martin <thi.martin.pro@pm.me> Date: Tue, 12 Sep 2023 15:46:06 +0200 Subject: [PATCH] Fix typo --- src/kernel_services/ast_data/annotations.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/kernel_services/ast_data/annotations.mli b/src/kernel_services/ast_data/annotations.mli index 435cbea2d60..3320c0bec9c 100644 --- a/src/kernel_services/ast_data/annotations.mli +++ b/src/kernel_services/ast_data/annotations.mli @@ -342,7 +342,7 @@ val add_spec: ?register_children:bool -> ?force:bool -> spec contract_component_addition (** Add new spec into the given contract. The [force] (which defaults to [false]) parameter is used to determine whether [decreases] and [terminates] - clauses mùst be relaced if they already exists and a new one is provided. + clauses must be replaced if they already exist and a new one is provided. More precisely, if [force] is [true] *and* the new contract has [Some terminates], the old one is removed and the new clause is used -- GitLab