From 0c1dfd77d4a6a0a929e62183d2b7b5da80847a05 Mon Sep 17 00:00:00 2001
From: Asma Tafat-Bouzid <atafat@lri.fr>
Date: Tue, 11 Oct 2011 15:26:33 +0200
Subject: [PATCH] Latex documentation
---
doc/manpages.tex | 6 ++++++
.../proofs/heap_Heap_Is_heap_relation_1.v | 4 +---
.../proofs/heapsort_WP_HeapSort_Min_of_sorted_1.v | 4 +---
3 files changed, 8 insertions(+), 6 deletions(-)
diff --git a/doc/manpages.tex b/doc/manpages.tex
index cd1a5e0dc1..8cf32f0449 100644
--- a/doc/manpages.tex
+++ b/doc/manpages.tex
@@ -496,6 +496,12 @@ not and you have to use the IDE to update it.
HTML syntax.
\end{itemize}
+About \texttt{latex} output, we propose another option
+\texttt{-latex2} with the same parameters. The difference between
+these two options is the layout of the tabular.
+
+Generated \latex files contain a set of macros. Definitions of these macros is left to the care of user depending on what he wants, or not, highlight.
+
\section{The \texttt{why3.conf} configuration file}
\label{sec:whyconffile}
One can use a custom configuration file. \texttt{why3config}
diff --git a/examples/programs/vacid_0_binary_heaps/proofs/heap_Heap_Is_heap_relation_1.v b/examples/programs/vacid_0_binary_heaps/proofs/heap_Heap_Is_heap_relation_1.v
index cdd4d7f312..c1b2be51c5 100644
--- a/examples/programs/vacid_0_binary_heaps/proofs/heap_Heap_Is_heap_relation_1.v
+++ b/examples/programs/vacid_0_binary_heaps/proofs/heap_Heap_Is_heap_relation_1.v
@@ -133,6 +133,4 @@ assert (h: x=0 \/ 0 < x) by omega.
apply Parent_inf_el with (n := n);
auto with zarith.
Qed.
-(* DO NOT EDIT BELOW *)
-
-
+(* DO NOT EDIT BELOW *)
\ No newline at end of file
diff --git a/examples/programs/vacid_0_binary_heaps/proofs/heapsort_WP_HeapSort_Min_of_sorted_1.v b/examples/programs/vacid_0_binary_heaps/proofs/heapsort_WP_HeapSort_Min_of_sorted_1.v
index 32ffb74612..680eee3dce 100644
--- a/examples/programs/vacid_0_binary_heaps/proofs/heapsort_WP_HeapSort_Min_of_sorted_1.v
+++ b/examples/programs/vacid_0_binary_heaps/proofs/heapsort_WP_HeapSort_Min_of_sorted_1.v
@@ -317,6 +317,4 @@ assert (h: (i = j-1 \/ i < j-1)%Z) by omega.
rewrite H_induc; auto with zarith.
unfold sorted_sub; auto with zarith.
Qed.
-(* DO NOT EDIT BELOW *)
-
-
+(* DO NOT EDIT BELOW *)
\ No newline at end of file
--
GitLab