From e12110637730d067c216abcc86185b761189b342 Mon Sep 17 00:00:00 2001
From: vblot <24938579+vblot@users.noreply.github.com>
Date: Fri, 28 May 2021 18:29:37 +0200
Subject: getting rid of native-coq (#95)

---
 INSTALL.md | 41 +----------------------------------------
 1 file changed, 1 insertion(+), 40 deletions(-)

(limited to 'INSTALL.md')

diff --git a/INSTALL.md b/INSTALL.md
index eb90daf..90b5cf5 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -81,12 +81,6 @@ You need to have OCaml version >= 4.08 and < 4.10 and Coq version 8.10.*.
 > SMTCoq. In particular this means you want a version of Coq that was compiled
 > with OCaml version >= 4.08.
 
-If you want to use SMTCoq with high performance to check large proof
-certificates, you need to use the [version of Coq with native
-data-structures](https://github.com/smtcoq/native-coq) instead of
-Coq-8.10 (warning: this allows one to use the vernacular commands but not
-the tactics).
-
 ### Install opam
 
 We recommended to install the required packages from
@@ -139,44 +133,11 @@ but you might need to install some extra packages and libraries for your system
 Compile and install SMTCoq by using the following commands in the src directory.
 
 ```bash
-./configure.sh
-make
-make install
-```
-
-## Installation with native-coq (not recommended except for high performances)
-
-> **Warning**: this installation procedure is recommended only to use
-> the vernacular commands efficiently (in particular, to check very
-> large proof certificates). It does not allow one to use the tactics.
-
-1. Download the git version of Coq with native compilation:
-```bash
-git clone https://github.com/smtcoq/native-coq.git
-```
-   and compile it by following the instructions available in the
-   repository. We recommand that you do not install it, but only compile
-   it in local:
-```bash
-./configure -local
-make
-```
-
-2. Set an environment variable COQBIN to the directory where Coq's
-   binaries are; for instance:
-```bash
-export COQBIN=/home/jdoe/native-coq/bin/
-```
-   (the final slash is mandatory).
-
-3. Compile and install SMTCoq by using the following commands in the src directory.
-```
-./configure.sh -native
+coq_makefile -f _CoqProject -o Makefile
 make
 make install
 ```
 
-
 ## Installation of the provers
 
 To use SMTCoq, we recommend installing the following two SMT solvers:
-- 
cgit 


From b40fefbb52afbc7deaa0b591d155bf2e84d0afba Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Fri, 28 May 2021 18:41:30 +0200
Subject: Add Makefile

---
 INSTALL.md | 1 -
 1 file changed, 1 deletion(-)

(limited to 'INSTALL.md')

diff --git a/INSTALL.md b/INSTALL.md
index 90b5cf5..940b2d5 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -133,7 +133,6 @@ but you might need to install some extra packages and libraries for your system
 Compile and install SMTCoq by using the following commands in the src directory.
 
 ```bash
-coq_makefile -f _CoqProject -o Makefile
 make
 make install
 ```
-- 
cgit