Final updates to the current documentation

3 files changed, 18 insertions, 18 deletions

diff --git a/src/Compiler.v b/src/Compiler.v
index 7aef71c..8882686 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -68,7 +68,7 @@ Require Import vericert.hls.HTLgenproof.
 (** ** Declarations
 
 We then need to declare the external OCaml functions used to print out intermediate steps in the
-compilation, such as ``print_RTL``, ``print_HTL`` and ``print_RTLBlock``.  *)
+compilation, such as [print_RTL], [print_HTL] and [print_RTLBlock].  *)
 
 Parameter print_RTL: Z -> RTL.program -> unit.
 Parameter print_HTL: Z -> HTL.program -> unit.
@@ -158,7 +158,7 @@ Qed.
 
 (** *** Top-level Translation
 
-An optimised transformation function from ``RTL`` to ``Verilog`` can then be defined, which applies
+An optimised transformation function from [RTL] to [Verilog] can then be defined, which applies
 the front end compiler optimisations of CompCert to the RTL that is generated and then performs the
 two Vericert passes from RTL to HTL and then from HTL to Verilog.  *)
 
@@ -236,7 +236,7 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
 
 (** ** Correctness Proof
 
-Finally, the top-level definition for all the passes is defined, which combines the ``match_prog``
+Finally, the top-level definition for all the passes is defined, which combines the [match_prog]
 predicates of each translation pass from C until Verilog.  *)
 
 Local Open Scope linking_scope.
@@ -260,14 +260,14 @@ Definition CompCert's_passes :=
   ::: mkpass Veriloggenproof.match_prog
   ::: pass_nil _.
 
-(** These passes are then composed into a larger, top-level ``match_prog`` predicate which matches a
+(** These passes are then composed into a larger, top-level [match_prog] predicate which matches a
 C program directly with a Verilog program.  *)
 
 Definition match_prog: Csyntax.program -> Verilog.program -> Prop :=
   pass_match (compose_passes CompCert's_passes).
 
 (** We then need to prove that this predicate holds, assuming that the translation is performed
-using the ``transf_hls`` function declared above.  *)
+using the [transf_hls] function declared above.  *)
 
 Theorem transf_hls_match:
   forall p tp,
@@ -373,8 +373,8 @@ Qed.
 
 The following theorem is a *backward simulation* between the C and Verilog, which proves the
 semantics preservation of the translation.  We can assume that the C and Verilog programs match, as
-we have proven previously in ``transf_hls_match`` that our translation implies that the
-``match_prog`` predicate will hold.  *)
+we have proven previously in [transf_hls_match] that our translation implies that the
+[match_prog] predicate will hold.  *)
 
 Theorem c_semantic_preservation:
   forall p tp,
@@ -391,8 +391,8 @@ Proof.
   exact (proj2 (cstrategy_semantic_preservation _ _ H)).
 Qed.
 
-(** We can then use ``transf_hls_match`` to prove the backward simulation where the assumption is
-that the translation is performed using the ``transf_hls`` function and that it succeeds.  *)
+(** We can then use [transf_hls_match] to prove the backward simulation where the assumption is
+that the translation is performed using the [transf_hls] function and that it succeeds.  *)
 
 Theorem transf_c_program_correct:
   forall p tp,
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v
index 9930f4d..bf4b057 100644
--- a/src/hls/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -1008,12 +1008,12 @@ Section CORRECTNESS.
       is a simulation argument based on diagrams of the following form:
 <<
                       match_states
-    code st rs ---------------- State m st assoc
-         ||                             |
-         ||                             |
-         ||                             |
-         \/                             v
-    code st rs' --------------- State m st assoc'
+    code st rs ------------------------- State m st assoc
+         ||                                      |
+         ||                                      |
+         ||                                      |
+         \/                                      v
+    code st rs' ------------------------ State m st assoc'
                       match_states
 >>
       where [tr_code c data control fin rtrn st] is assumed to hold.
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index 7eabcf7..52259a0 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -33,15 +33,15 @@ Require Import Vericertlib.
 
 (** * RTLBlock Instructions
 
-These instructions are used for ``RTLBlock`` and ``RTLPar``, so that they have consistent
+These instructions are used for [RTLBlock] and [RTLPar], so that they have consistent
 instructions, which greatly simplifies the proofs, as they will by default have the same instruction
 syntax and semantics.  The only changes are therefore at the top-level of the instructions.
 
 ** Instruction Definition
 
 First, we define the instructions that can be placed into a basic block, meaning they won't branch.
-The main changes to how instructions are defined in ``RTL``, is that these instructions don't have a
-next node, as they will be in a basic block, and they also have an optional predicate (``pred_op``).
+The main changes to how instructions are defined in [RTL], is that these instructions don't have a
+next node, as they will be in a basic block, and they also have an optional predicate ([pred_op]).
 *)
 
 Definition node := positive.