From 442622f32d667580cb7ad7c7edd0ecf75d2f6c92 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 21 Nov 2020 11:32:34 +0000 Subject: Update on Overleaf. --- main.tex | 2 +- proof.tex | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/main.tex b/main.tex index aab349a..0751276 100644 --- a/main.tex +++ b/main.tex @@ -56,7 +56,7 @@ \ANONYMOUStrue \newif\ifCOMMENTS -\COMMENTStrue +\COMMENTSfalse \newcommand{\Comment}[3]{\ifCOMMENTS\textcolor{#1}{{\bf [\![#2:} #3{\bf ]\!]}}\fi} \newcommand\JW[1]{\Comment{red!75!black}{JW}{#1}} \newcommand\YH[1]{\Comment{green!50!blue}{YH}{#1}} diff --git a/proof.tex b/proof.tex index 36b997b..9a4ab40 100644 --- a/proof.tex +++ b/proof.tex @@ -154,7 +154,7 @@ The final lemma we need is that the Verilog we generate is deterministic. This r \begin{table*} \centering - \begin{tabular}{llllll} + \begin{tabular}{lrrrrr} \toprule & \textbf{Coq code} & \textbf{OCaml code} & \textbf{Specifications} & \textbf{Theorems \& Proofs} & \textbf{Total}\\ \midrule -- cgit