diff --git a/src/kernel_services/ast_data/annotations.mli b/src/kernel_services/ast_data/annotations.mli index 435cbea2d600ee79a762a93fdcb8eabea37cb38c..3320c0bec9c80ca7fb21a1ce87034a4b2cba3aa3 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