Merge remote-tracking branch 'origin/new-assigns-check' into new-assi…

…gns-check
model-checking · Dec 23, 2023 · 0819432 · 0819432
2 parents 6892afc + c5b6a2b
commit 0819432
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
@@ -588,7 +588,7 @@ macro_rules! comma_tok {
  };
 }
 
-/// Parse the a token stream inside an attribute (like `kanitool::modifies`) as a comma separated
+/// Parse the token stream inside an attribute (like `kanitool::modifies`) as a comma separated
 /// sequence of function parameter names on `local_def_id` (must refer to a function). Then
 /// translates the names into [`Local`]s.
 fn parse_modify_values<'a>(

diff --git a/library/kani/src/contracts.rs b/library/kani/src/contracts.rs
@@ -118,7 +118,7 @@
 //!
 //! ## Specification Attributes Overview
 //!
-//! The basic two two specification attributes available for describing
+//! The basic two specification attributes available for describing
 //! function behavior are [`requires`][macro@requires] for preconditions and
 //! [`ensures`][macro@ensures] for postconditions. Both admit arbitrary Rust
 //! expressions as their bodies which may also reference the function arguments