Merge remote-tracking branch 'origin/master'

1 files changed, 1 insertions, 1 deletions

diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex
index 4c403fc..3b6313b 100644
--- a/verified_resource_sharing.tex
+++ b/verified_resource_sharing.tex
@@ -124,7 +124,7 @@ It transforms its input through a series of ten intermediate languages before ge
 %This design ensures that each individual pass remains relatively simple and hence feasible to prove correct.
 The correctness proof of the entire compiler is formed by composing the correctness proofs of each of those passes. 
 \YHchanged{That the Csmith compiler testing tool}~\cite{csmith} has found hundreds of bugs in GCC and LLVM but none in (the verified parts of) CompCert is a testament to the reliability of this development approach. 
-\YHchanged{However, we} cannot guarantee \vericertfun{} designs will never go wrong, because of fallible components not covered by the theorem, such as the synthesis toolchain~\cite{verismith} and the FPGA itself.
+\YHchanged{In \vericertfun{} designs, however, we cannot guarantee that they will never go wrong, because of fallible components not covered by the theorem, such as the synthesis toolchain~\cite{verismith} and the FPGA itself.}
  
 \paragraph{The \vericert{} verified HLS tool}