Now, Coq 8.5 is the default

11 files changed, 119 insertions, 477 deletions

diff --git a/INSTALL.md b/INSTALL.md
index e97bed4..0c6bd1e 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -9,8 +9,41 @@ amd64).
 
 ## Installation from the sources
 
-Currently, SMTCoq can be built only from the sources, using the
-[version of Coq with native data-structures](https://github.com/smtcoq/native-coq). The design of an opam package is under progress.
+Currently, SMTCoq can be built only from the sources, using either Coq 8.5 or the
+[version of Coq with native data-structures](https://github.com/smtcoq/native-coq). The design of an opam package is under progress. We recommend Coq 8.5 for standard use, and native-coq for uses that require very efficient computation. In both cases, you will need to install the provers (see below).
+
+
+### Installation with Coq 8.5
+
+1. Download the last stable version of Coq 8.5:
+```
+wget https://coq.inria.fr/distrib/V8.5pl1/files/coq-8.5pl1.tar.gz
+```
+   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:
+```
+./configure -local
+make
+```
+
+2. Set an environment variable COQBIN to the directory where Coq's
+   binaries are; for instance:
+```
+export COQBIN=/home/jdoe/woe-8.5pl1/bin/
+```
+   (the final slash is mandatory).
+
+3. Compile and install SMTCoq by using the commands:
+```
+./configure.sh
+make
+make install
+```
+   in the src directory.
+
+
+### Installation with native-coq
 
 1. Download the git version of Coq with native compilation:
 ```
@@ -33,6 +66,7 @@ export COQBIN=/home/jdoe/native-coq/bin/
 
 3. Compile and install SMTCoq by using the commands:
 ```
+./configure.sh -native
 make
 make install
 ```
diff --git a/README.md b/README.md
index 8fcdd33..4e960d6 100644
--- a/README.md
+++ b/README.md
@@ -152,18 +152,3 @@ forall l, b1 = b2
 where `l` is a list of Booleans. Those Booleans can be any concrete
 terms. The theories that are currently supported are `QF_UF`, `QF_LIA`,
 `QF_IDL` and their combinations.
-
-
-#### Extraction
-
-The `src/extraction` directory contains the OCaml extracted checker, as
-well as additional files to make use of it. You can compile it using the
-given `Makefile` (after compiling SMTCoq): it will produce an executable
-`smtcoq` that can be run independently of SMTCoq in this way:
-- `smtcoq -zchaff foo.cnf foo.zlog` runs the ZChaff checker on a DIMACS
-  file and the corresponding ZChaff certificate
-- `smtcoq -verit foo.smt2 foo.vtlog` runs the veriT checker on a SMTLIB2
-  file and the corresponding veriT certificate.
-
-Note that even the extracted version of SMTCoq requires both native-coq
-and SMTCoq to be compiled (mainly since it relies on other Coq plugins).
diff --git a/src/Makefile b/src/Makefile
deleted file mode 100644
index c7ac7c5..0000000
--- a/src/Makefile
+++ /dev/null
@@ -1,436 +0,0 @@
-#############################################################################
-##  v      #                   The Coq Proof Assistant                     ##
-## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##
-##   \VV/  #                                                               ##
-##    //   #  Makefile automagically generated by coq_makefile Vtrunk      ##
-#############################################################################
-
-# WARNING
-#
-# This Makefile has been automagically generated
-# Edit at your own risks !
-#
-# END OF WARNING
-
-#
-# This Makefile was generated by the command line :
-# coq_makefile -f Make -o Makefile 
-#
-
-.DEFAULT_GOAL := all
-
-# 
-# This Makefile may take arguments passed as environment variables:
-# COQBIN to specify the directory where Coq binaries resides;
-# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;
-# DSTROOT to specify a prefix to install path.
-
-# Here is a hack to make $(eval $(shell works:
-define donewline
-
-
-endef
-includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr '\n' '@'; })))
-$(call includecmdwithout@,$(COQBIN)coqtop -config)
-
-##########################
-#                        #
-# Libraries definitions. #
-#                        #
-##########################
-
-OCAMLLIBS?=-I versions/native\
-  -I zchaff\
-  -I verit\
-  -I trace\
-  -I smtlib2\
-  -I lia\
-  -I euf\
-  -I cnf
-COQLIBS?=-I versions/native\
-  -I zchaff\
-  -I verit\
-  -I trace\
-  -I smtlib2\
-  -I lia\
-  -I euf\
-  -I cnf -R . SMTCoq
-COQDOCLIBS?=-R . SMTCoq
-
-##########################
-#                        #
-# Variables definitions. #
-#                        #
-##########################
-
-CAMLYACC=$(CAMLBIN)ocamlyacc
-CAMLLEX=$(CAMLBIN)ocamllex
-VCMXS=NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Assumptions.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmi spl/NSMTCoq_spl_Assumptions.cmi spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_SMTCoq.cmi
-CMXS=trace/smt_tactic.cmxs
-CMXA=trace/smtcoq.cmxa
-
-OPT?=
-COQDEP?=$(COQBIN)coqdep -c
-COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
-COQCHKFLAGS?=-silent -o
-COQDOCFLAGS?=-interpolate -utf8
-COQC?=$(COQBIN)coqc
-GALLINA?=$(COQBIN)gallina
-COQDOC?=$(COQBIN)coqdoc
-COQCHK?=$(COQBIN)coqchk
-
-COQSRCLIBS?=-I $(COQLIB)kernel -I $(COQLIB)lib \
-  -I $(COQLIB)library -I $(COQLIB)parsing \
-  -I $(COQLIB)pretyping -I $(COQLIB)interp \
-  -I $(COQLIB)proofs -I $(COQLIB)tactics \
-  -I $(COQLIB)toplevel \
-  -I $(COQLIB)plugins/btauto \
-  -I $(COQLIB)plugins/cc \
-  -I $(COQLIB)plugins/decl_mode \
-  -I $(COQLIB)plugins/extraction \
-  -I $(COQLIB)plugins/field \
-  -I $(COQLIB)plugins/firstorder \
-  -I $(COQLIB)plugins/fourier \
-  -I $(COQLIB)plugins/funind \
-  -I $(COQLIB)plugins/micromega \
-  -I $(COQLIB)plugins/nsatz \
-  -I $(COQLIB)plugins/omega \
-  -I $(COQLIB)plugins/quote \
-  -I $(COQLIB)plugins/ring \
-  -I $(COQLIB)plugins/romega \
-  -I $(COQLIB)plugins/rtauto \
-  -I $(COQLIB)plugins/setoid_ring \
-  -I $(COQLIB)plugins/syntax \
-  -I $(COQLIB)plugins/xml
-ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)
-
-CAMLC?=$(OCAMLC) -c -rectypes
-CAMLOPTC?=$(OCAMLOPT) -c -rectypes
-CAMLLINK?=$(OCAMLC) -rectypes
-CAMLOPTLINK?=$(OCAMLOPT) -rectypes
-GRAMMARS?=grammar.cma
-CAMLP4EXTEND?=pa_extend.cmo pa_macro.cmo q_MLast.cmo
-CAMLP4OPTIONS?=-loc loc
-PP?=-pp "$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl"
-
-##################
-#                #
-# Install Paths. #
-#                #
-##################
-
-ifdef USERINSTALL
-XDG_DATA_HOME?=$(HOME)/.local/share
-COQLIBINSTALL=$(XDG_DATA_HOME)/coq
-COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq
-else
-COQLIBINSTALL=${COQLIB}user-contrib
-COQDOCINSTALL=${DOCDIR}user-contrib
-endif
-
-######################
-#                    #
-# Files dispatching. #
-#                    #
-######################
-
-VFILES:=Trace.v\
-  State.v\
-  SMT_terms.v\
-  SMTCoq.v\
-  Misc.v\
-  spl/Operators.v\
-  spl/Arithmetic.v\
-  spl/Syntactic.v\
-  spl/Assumptions.v\
-  lia/Lia.v\
-  euf/Euf.v\
-  cnf/Cnf.v
-
--include $(addsuffix .d,$(VFILES))
-.SECONDARY: $(addsuffix .d,$(VFILES))
-
-vo_to_obj = $(addsuffix .o,$(foreach vo,$(1),$(addprefix $(dir $(vo)),$(filter-out Warning: Error:,$(firstword $(shell $(COQBIN)coqtop -batch -quiet -print-mod-uid $(vo:.vo=)))))))
-VOFILES:=$(foreach vo,$(VFILES:.v=.vo),$(dir $(vo))$(notdir $(vo)))
-GLOBFILES:=$(VFILES:.v=.glob)
-VIFILES:=$(VFILES:.v=.vi)
-GFILES:=$(VFILES:.v=.g)
-HTMLFILES:=$(VFILES:.v=.html)
-GHTMLFILES:=$(VFILES:.v=.g.html)
-OBJFILES:=$(call vo_to_obj,$(VOFILES))
-ML4FILES:=trace/smt_tactic.ml4
-
--include $(addsuffix .d,$(ML4FILES))
-.SECONDARY: $(addsuffix .d,$(ML4FILES))
-
-MLFILES:=lia/lia.ml\
-  zchaff/zchaffParser.ml\
-  zchaff/zchaff.ml\
-  zchaff/satParser.ml\
-  zchaff/cnfParser.ml\
-  verit/veritSyntax.ml\
-  verit/verit.ml\
-  verit/veritLexer.ml\
-  verit/veritParser.ml\
-  smtlib2/smtlib2_util.ml\
-  smtlib2/smtlib2_genConstr.ml\
-  smtlib2/smtlib2_ast.ml\
-  smtlib2/smtlib2_lex.ml\
-  smtlib2/smtlib2_parse.ml\
-  trace/smtTrace.ml\
-  trace/smtMisc.ml\
-  trace/smtForm.ml\
-  trace/smtCommands.ml\
-  trace/smtCnf.ml\
-  trace/smtCertif.ml\
-  trace/smtAtom.ml\
-  trace/satAtom.ml\
-  trace/coqTerms.ml\
-  versions/native/structures.ml
-
--include $(addsuffix .d,$(MLFILES))
-.SECONDARY: $(addsuffix .d,$(MLFILES))
-
-MLIFILES:=verit/veritSyntax.mli\
-  trace/smtForm.mli\
-  trace/smtAtom.mli
-
--include $(addsuffix .d,$(MLIFILES))
-.SECONDARY: $(addsuffix .d,$(MLIFILES))
-
-ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo)
-CMOFILES=$(filter-out $(addsuffix .cmo,$(foreach lib,$(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES) $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ALLCMOFILES))
-CMXFILES=$(CMOFILES:.cmo=.cmx)
-CMIFILES=$(sort $(ALLCMOFILES:.cmo=.cmi) $(MLIFILES:.mli=.cmi))
-CMXSFILES=$(CMXFILES:.cmx=.cmxs)
-
-#######################################
-#                                     #
-# Definition of the toplevel targets. #
-#                                     #
-#######################################
-
-all: ml $(CMXFILES) $(CMXA) $(CMXS) $(VOFILES)
-
-mlihtml: $(MLIFILES:.mli=.cmi)
-	 mkdir $@ || rm -rf $@/*
-	$(OCAMLDOC) -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)
-
-all-mli.tex: $(MLIFILES:.mli=.cmi)
-	$(OCAMLDOC) -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)
-
-spec: $(VIFILES)
-
-gallina: $(GFILES)
-
-html: $(GLOBFILES) $(VFILES)
-	- mkdir -p html
-	$(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)
-
-gallinahtml: $(GLOBFILES) $(VFILES)
-	- mkdir -p html
-	$(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)
-
-all.ps: $(VFILES)
-	$(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-all-gal.ps: $(VFILES)
-	$(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-all.pdf: $(VFILES)
-	$(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-all-gal.pdf: $(VFILES)
-	$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-validate: $(VOFILES)
-	$(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=))
-
-beautify: $(VFILES:=.beautified)
-	for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
-	@echo 'Do not do "make clean" until you are sure that everything went well!'
-	@echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/'
-
-.PHONY: all opt byte archclean clean install userinstall depend html validate
-
-###################
-#                 #
-# Custom targets. #
-#                 #
-###################
-
-$(CMXS): $(CMXA)
-	$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^
-
-$(CMXA): versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx trace/smt_tactic.cmx
-	$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^
-
-ml: verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml
-
-
-%.ml %.mli: %.mly
-	$(CAMLYACC) $<
-
-%.ml: %.mll
-	$(CAMLLEX) $<
-
-vtest: 
-	cd ../unit-tests; make verit
-
-ztest: 
-	cd ../unit-tests; make zchaff
-
-test: 
-	cd ../unit-tests; make
-
-####################
-#                  #
-# Special targets. #
-#                  #
-####################
-
-byte:
-	$(MAKE) all "OPT:=-byte"
-
-opt:
-	$(MAKE) all "OPT:=-opt"
-
-userinstall:
-	+$(MAKE) USERINSTALL=true install
-
-install-natdynlink:
-	for i in $(CMXS); do \
-	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
-	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
-	done
-	for i in $(CMXA); do \
-	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
-	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
-	done
-	for i in $(VCMXS); do \
-	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
-	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
-	done
-
-install:$(if ifeq '$(HASNATDYNLINK)' 'true',install-natdynlink)
-	for i in $(VOFILES) $(OBJFILES) $(OBJFILES:.o=.cm*); do \
-	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
-	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
-	done
-	for i in $(CMXFILES); do \
-	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
-	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
-	done
-	for i in $(CMIFILES); do \
-	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
-	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
-	done
-
-install-doc:
-	install -d $(DSTROOT)$(COQDOCINSTALL)/SMTCoq/html
-	for i in html/*; do \
-	 install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/SMTCoq/$$i;\
-	done
-	install -d $(DSTROOT)$(COQDOCINSTALL)/SMTCoq/mlihtml
-	for i in mlihtml/*; do \
-	 install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/SMTCoq/$$i;\
-	done
-
-clean:
-	rm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES)
-	rm -f $(ALLCMOFILES:.cmo=.cmx) $(CMXAFILES) $(CMXSFILES) $(ALLCMOFILES:.cmo=.o) $(CMXAFILES:.cmxa=.a)
-	rm -f $(addsuffix .d,$(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(MLPACKFILES))
-	rm -f $(OBJFILES) $(OBJFILES:.o=.native)
-	rm -f $(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo)
-	rm -f $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)
-	rm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)
-	rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex
-	- rm -rf html mlihtml
-	- rm -rf $(CMXS)
-	- rm -rf $(CMXA)
-	- rm -rf ml
-	- rm -rf vtest
-	- rm -rf ztest
-	- rm -rf test
-	- rm -f NSMTCoq* cnf/NSMTCoq* euf/NSMTCoq* lia/NSMTCoq* spl/NSMTCoq* ../unit-tests/NSMTCoq* ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.mli smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml
-
-archclean:
-	rm -f *.cmx *.o
-
-printenv:
-	@$(COQBIN)coqtop -config
-	@echo CAMLC =	$(CAMLC)
-	@echo CAMLOPTC =	$(CAMLOPTC)
-	@echo PP =	$(PP)
-	@echo COQFLAGS =	$(COQFLAGS)
-	@echo COQLIBINSTALL =	$(COQLIBINSTALL)
-	@echo COQDOCINSTALL =	$(COQDOCINSTALL)
-
-
-###################
-#                 #
-# Implicit rules. #
-#                 #
-###################
-
-%.cmi: %.mli
-	$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<
-
-%.mli.d: %.mli
-	$(OCAMLDEP) -slash $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
-
-%.cmo: %.ml4
-	$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<
-
-%.cmx: %.ml4
-	$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<
-
-%.ml4.d: %.ml4
-	$(OCAMLDEP) -slash $(OCAMLLIBS) $(PP) -impl "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
-
-%.cmo: %.ml
-	$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<
-
-%.cmx: %.ml
-	$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<
-
-%.ml.d: %.ml
-	$(OCAMLDEP) -slash $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
-
-%.cmxs: %.cmx
-	$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<
-
-%.vo %.glob: %.v
-	$(COQC) $(COQDEBUG) $(COQFLAGS) $*
-
-%.vi: %.v
-	$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
-
-%.g: %.v
-	$(GALLINA) $<
-
-%.tex: %.v
-	$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
-
-%.html: %.v %.glob
-	$(COQDOC) $(COQDOCFLAGS) -html $< -o $@
-
-%.g.tex: %.v
-	$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
-
-%.g.html: %.v %.glob
-	$(COQDOC)$(COQDOCFLAGS)  -html -g $< -o $@
-
-%.v.d: %.v
-	$(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
-
-%.v.beautified:
-	$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*
-
-# WARNING
-#
-# This Makefile has been automagically generated
-# Edit at your own risks !
-#
-# END OF WARNING
-
diff --git a/src/SMTCoq.v b/src/SMTCoq.v
index 40ef316..b6a9871 100644
--- a/src/SMTCoq.v
+++ b/src/SMTCoq.v
@@ -18,4 +18,4 @@ Require Export Int63 List PArray.
 Require Export State SMT_terms Trace.
 Export Atom Form Sat_Checker Cnf_Checker Euf_Checker.
 
-Declare ML Module "trace/smt_tactic".
+Declare ML Module "smtcoq_plugin".
diff --git a/src/configure.sh b/src/configure.sh
index 83b70d3..dfa86ab 100755
--- a/src/configure.sh
+++ b/src/configure.sh
@@ -2,8 +2,12 @@
 
 set -e
 
-if [ $@ -a $@ = -standard ]; then
+if [ $@ -a $@ = -native ]; then
+    cp versions/native/Makefile Makefile
+    cp versions/native/smtcoq_plugin_native.ml4 smtcoq_plugin.ml4
+else
     cp versions/standard/Makefile Makefile
+    cp versions/standard/smtcoq_plugin_standard.ml4 smtcoq_plugin.ml4
     cp versions/standard/Int63/Int63_standard.v versions/standard/Int63/Int63.v
     cp versions/standard/Int63/Int63Lib_standard.v versions/standard/Int63/Int63Lib.v
     cp versions/standard/Int63/Cyclic63_standard.v versions/standard/Int63/Cyclic63.v
@@ -13,6 +17,4 @@ if [ $@ -a $@ = -standard ]; then
     cp versions/standard/Int63/Int63Axioms_standard.v versions/standard/Int63/Int63Axioms.v
     cp versions/standard/Int63/Int63Properties_standard.v versions/standard/Int63/Int63Properties.v
     cp versions/standard/Array/PArray_standard.v versions/standard/Array/PArray.v
-else
-    cp versions/native/Makefile Makefile
 fi
diff --git a/src/versions/native/Make b/src/versions/native/Make
index 5659cc7..2b81917 100644
--- a/src/versions/native/Make
+++ b/src/versions/native/Make
@@ -37,11 +37,11 @@
 -custom "$(CAMLYACC) $<" "%.mly" "%.ml %.mli"
 -custom "" "verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml" "ml"
 
--custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx trace/smt_tactic.cmx" "$(CMXA)"
+-custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx smtcoq_plugin.cmx" "$(CMXA)"
 -custom "$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^" "$(CMXA)" "$(CMXS)"
 
-CMXA = trace/smtcoq.cmxa
-CMXS = trace/smt_tactic.cmxs
+CMXA = smtcoq.cmxa
+CMXS = smtcoq_plugin.cmxs
 VCMXS = "NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Assumptions.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmi spl/NSMTCoq_spl_Assumptions.cmi spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_SMTCoq.cmi"
 CAMLLEX = $(CAMLBIN)ocamllex
 CAMLYACC = $(CAMLBIN)ocamlyacc
@@ -58,7 +58,6 @@ trace/smtCommands.ml
 trace/smtForm.ml
 trace/smtForm.mli
 trace/smtMisc.ml
-trace/smt_tactic.ml4
 trace/smtTrace.ml
 
 smtlib2/smtlib2_parse.ml
@@ -95,3 +94,5 @@ SMTCoq.v
 SMT_terms.v
 State.v
 Trace.v
+
+smtcoq_plugin.ml4
diff --git a/src/versions/native/Makefile b/src/versions/native/Makefile
index c7ac7c5..958b64f 100644
--- a/src/versions/native/Makefile
+++ b/src/versions/native/Makefile
@@ -66,8 +66,8 @@ COQDOCLIBS?=-R . SMTCoq
 CAMLYACC=$(CAMLBIN)ocamlyacc
 CAMLLEX=$(CAMLBIN)ocamllex
 VCMXS=NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Assumptions.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmi spl/NSMTCoq_spl_Assumptions.cmi spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_SMTCoq.cmi
-CMXS=trace/smt_tactic.cmxs
-CMXA=trace/smtcoq.cmxa
+CMXS=smtcoq_plugin.cmxs
+CMXA=smtcoq.cmxa
 
 OPT?=
 COQDEP?=$(COQBIN)coqdep -c
@@ -158,7 +158,7 @@ GFILES:=$(VFILES:.v=.g)
 HTMLFILES:=$(VFILES:.v=.html)
 GHTMLFILES:=$(VFILES:.v=.g.html)
 OBJFILES:=$(call vo_to_obj,$(VOFILES))
-ML4FILES:=trace/smt_tactic.ml4
+ML4FILES:=smtcoq_plugin.ml4
 
 -include $(addsuffix .d,$(ML4FILES))
 .SECONDARY: $(addsuffix .d,$(ML4FILES))
@@ -262,7 +262,7 @@ beautify: $(VFILES:=.beautified)
 $(CMXS): $(CMXA)
 	$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^
 
-$(CMXA): versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx trace/smt_tactic.cmx
+$(CMXA): versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx smtcoq_plugin.cmx
 	$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^
 
 ml: verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml
diff --git a/src/versions/native/smtcoq_plugin_native.ml4 b/src/versions/native/smtcoq_plugin_native.ml4
new file mode 100644
index 0000000..e7c2f5b
--- /dev/null
+++ b/src/versions/native/smtcoq_plugin_native.ml4
@@ -0,0 +1,56 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2016                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - Université Paris-Sud                 *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+VERNAC COMMAND EXTEND Vernac_zchaff
+| [ "Parse_certif_zchaff" 
+    ident(dimacs) ident(trace) string(fdimacs) string(fproof) ] ->
+  [
+    Zchaff.parse_certif dimacs trace fdimacs fproof
+  ]
+| [ "Zchaff_Checker" string(fdimacs) string(fproof) ] ->
+  [
+    Zchaff.checker fdimacs fproof
+  ]
+| [ "Zchaff_Theorem" ident(name) string(fdimacs) string(fproof) ] ->
+  [
+    Zchaff.theorem name fdimacs fproof
+  ]
+END
+
+VERNAC COMMAND EXTEND Vernac_verit
+| [ "Parse_certif_verit"
+    ident(t_i) ident(t_func) ident(t_atom) ident(t_form) ident(root) ident(used_roots) ident(trace) string(fsmt) string(fproof) ] ->
+  [
+    Verit.parse_certif t_i t_func t_atom t_form root used_roots trace fsmt fproof
+  ]
+| [ "Verit_Checker" string(fsmt) string(fproof) ] ->
+  [
+    Verit.checker fsmt fproof
+  ]
+| [ "Verit_Theorem" ident(name) string(fsmt) string(fproof) ] ->
+  [
+    Verit.theorem name fsmt fproof
+  ]
+END
+
+
+TACTIC EXTEND Tactic_zchaff
+| [ "zchaff" ] -> [ Structures.mk_sat_tactic Zchaff.tactic ]
+END
+
+TACTIC EXTEND Tactic_verit
+| [ "verit" ] -> [ Structures.mk_smt_tactic Verit.tactic ]
+END
diff --git a/src/versions/standard/Make b/src/versions/standard/Make
index 42d0552..c833f4d 100644
--- a/src/versions/standard/Make
+++ b/src/versions/standard/Make
@@ -15,7 +15,7 @@
 ## Change the "install" target: change CMO into CMX.                  ##
 ## Remove the automatically generated line with %.cmxs: %.cmx         ##
 ## Finally, suppress the "Makefile" target and add to the "clean" target: ##
-##   - rm -f ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.mli smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml ##
+##   - rm -f ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.mli smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtcoq.a ##
 ########################################################################
 
 
@@ -40,11 +40,11 @@
 -custom "$(CAMLYACC) $<" "%.mly" "%.ml %.mli"
 -custom "" "verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml" "ml"
 
--custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "versions/standard/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx trace/smt_tactic.cmx" "$(CMXA)"
+-custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "versions/standard/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx smtcoq_plugin.cmx" "$(CMXA)"
 -custom "$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^" "$(CMXA)" "$(CMXS)"
 
-CMXA = trace/smtcoq.cmxa
-CMXS = trace/smt_tactic.cmxs
+CMXA = smtcoq.cmxa
+CMXS = smtcoq_plugin.cmxs
 CAMLLEX = $(CAMLBIN)ocamllex
 CAMLYACC = $(CAMLBIN)ocamlyacc
 
@@ -70,7 +70,6 @@ trace/smtCommands.ml
 trace/smtForm.ml
 trace/smtForm.mli
 trace/smtMisc.ml
-trace/smt_tactic.ml4
 trace/smtTrace.ml
 
 smtlib2/smtlib2_parse.ml
@@ -109,3 +108,5 @@ SMTCoq.v
 SMT_terms.v
 State.v
 Trace.v
+
+smtcoq_plugin.ml4
diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile
index cb92e59..da82e43 100644
--- a/src/versions/standard/Makefile
+++ b/src/versions/standard/Makefile
@@ -80,8 +80,8 @@ COQDOCLIBS?=\
 #                        #
 ##########################
 
-CMXA=trace/smtcoq.cmxa
-CMXS=trace/smt_tactic.cmxs
+CMXA=smtcoq.cmxa
+CMXS=smtcoq_plugin.cmxs
 CAMLLEX=$(CAMLBIN)ocamllex
 CAMLYACC=$(CAMLBIN)ocamlyacc
 
@@ -207,7 +207,7 @@ GHTMLFILES:=$(VFILES:.v=.g.html)
 OBJFILES=$(call vo_to_obj,$(VOFILES))
 ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)
 NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f))
-ML4FILES:=trace/smt_tactic.ml4
+ML4FILES:=smtcoq_plugin.ml4
 
 ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
 -include $(addsuffix .d,$(ML4FILES))
@@ -358,7 +358,7 @@ vtest:
 
 ml: verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml
 
-$(CMXA): versions/standard/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx trace/smt_tactic.cmx
+$(CMXA): versions/standard/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx smtcoq_plugin.cmx
 	$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^
 
 $(CMXS): $(CMXA)
@@ -477,7 +477,7 @@ clean::
 	- rm -rf ml
 	- rm -rf $(CMXA)
 	- rm -rf $(CMXS)
-	- rm -f ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.mli smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml
+	- rm -f ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.mli smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtcoq.a
 
 cleanall:: clean
 	rm -f $(patsubst %.v,.%.aux,$(VFILES))
diff --git a/src/trace/smt_tactic.ml4 b/src/versions/standard/smtcoq_plugin_standard.ml4
index d3fca95..3666ee1 100644
--- a/src/trace/smt_tactic.ml4
+++ b/src/versions/standard/smtcoq_plugin_standard.ml4
@@ -14,8 +14,7 @@
 (**************************************************************************)
 
 
-(* Uncomment for 8.5 *)
-(* DECLARE PLUGIN "trace/smt_tactic" *)
+DECLARE PLUGIN "smtcoq_plugin"
 
 VERNAC COMMAND EXTEND Vernac_zchaff
 | [ "Parse_certif_zchaff"