diff --git a/examples/mccarthy.mlw b/examples/mccarthy.mlw index 4346347e5d59d0f2f31c9e2c8a13b932e6a8ed6e..941af08c6ebbb94455233b97d724f4fb02f71319 100644 --- a/examples/mccarthy.mlw +++ b/examples/mccarthy.mlw @@ -1,5 +1,5 @@ -(** {1 McCarthy's ``91'' function} +(** {1 McCarthy's "91" function} authors: Jean-Christophe Filliâtre, Martin Clochard, Claude Marché witness: Andrei Paskevich diff --git a/examples/sumrange.mlw b/examples/sumrange.mlw index 3e89f74099f58901978f29ad4adf57052c7c9435..3cc7b22cece125b4744e6fdc335f83796a9ad499 100644 --- a/examples/sumrange.mlw +++ b/examples/sumrange.mlw @@ -348,7 +348,7 @@ module CumulativeTree So far, we are only able to prove that `update` is logarithmic - We express the complexity by passing a ``credit'' as a ghost + We express the complexity by passing a "credit" as a ghost parameter. We pose the precondition that the credit is at least equal to the depth of the tree. diff --git a/stdlib/ref.mlw b/stdlib/ref.mlw index 6284a0626aef1b607b68f029d0a8b6d20fa463c4..64e0c562f43906a33298df9208c7be8b194be3d8 100644 --- a/stdlib/ref.mlw +++ b/stdlib/ref.mlw @@ -1,7 +1,7 @@ (** {1 References} - A mutable variable, or ``reference'' in ML terminology, is simply a + A mutable variable, or "reference" in ML terminology, is simply a record with a single mutable field [contents]. *)