Commit 27af9602 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Avoid some backticks in documentation.

"\`\`" could have been used too, but it is a bit unreadable.
parent 19720359
(** {1 McCarthy's ``91'' function} (** {1 McCarthy's "91" function}
authors: Jean-Christophe Filliâtre, Martin Clochard, Claude Marché authors: Jean-Christophe Filliâtre, Martin Clochard, Claude Marché
witness: Andrei Paskevich witness: Andrei Paskevich
......
...@@ -348,7 +348,7 @@ module CumulativeTree ...@@ -348,7 +348,7 @@ module CumulativeTree
So far, we are only able to prove that `update` is logarithmic 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 parameter. We pose the precondition that the credit is at least
equal to the depth of the tree. equal to the depth of the tree.
......
(** {1 References} (** {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]. record with a single mutable field [contents].
*) *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment