From 7da3a3dc751adb2829c29b0b1500913636ba1f41 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Fri, 15 Mar 2019 13:27:56 +0100
Subject: Explain LFSCSIGS in the installation instructions for CVC4

---
 INSTALL.md | 38 +++++++++++++++++---------------------
 1 file changed, 17 insertions(+), 21 deletions(-)

(limited to 'INSTALL.md')

diff --git a/INSTALL.md b/INSTALL.md
index 5ad4ecb..1e908f9 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -186,6 +186,23 @@ the latest version available).
 
 The `cvc4` binary must be present in your PATH to use it through SMTCoq.
 
+In your `.bashrc` (or `.bash_profile`, or any other initialization file read by
+your shell), export the following environment variable to make it point at the
+`signatures` directory distributed with SMTCoq.
+
+> Don't use `~` in the path but rather `$HOME`.
+
+```bash
+export LFSCSIGS="$HOME/path/to/smtcoq/src/lfsc/tests/signatures/"
+```
+
+If you don't want SMTCoq to spit the translated proof in your proof environment
+window, add the following optional definition (in the same file).
+
+```bash
+export DONTSHOWVERIT="yes"
+```
+
 
 ### veriT
 
@@ -219,27 +236,6 @@ The `zchaff` binary must be present in your PATH to use it through SMTCoq.
 
 
 ## Setting up environment for SMTCoq
-
-To use the latest features of SMTCoq, you need to make these configuration
-changes:
-
-In your `.bashrc` (or `.bash_profile`, or any other initialization file read by
-your shell), export the following environment variable to make it point at the
-`signatures` directory distributed with SMTCoq.
-
-> Don't use `~` in the path but rather `$HOME`.
-
-```bash
-export LFSCSIGS="$HOME/path/to/smtcoq/src/lfsc/tests/signatures/"
-```
-
-If you don't want SMTCoq to spit the translated proof in your proof environment
-window, add the following optional definition (in the same file).
-
-```bash
-export DONTSHOWVERIT="yes"
-```
-
 ### Using SMTCoq without installing
 
 If you want to use SMTCoq without installing it your Coq installation, you can
-- 
cgit