From bfce2747a747f48465fe32c3d29304ca6e774f25 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Fri, 18 Mar 2016 18:01:20 +0100
Subject: Light port to Coq 8.5 under progress

---
 src/versions/native/Make          |  96 +++++++++
 src/versions/native/Makefile      | 435 ++++++++++++++++++++++++++++++++++++++
 src/versions/native/structures.ml |  72 +++++++
 3 files changed, 603 insertions(+)
 create mode 100644 src/versions/native/Make
 create mode 100644 src/versions/native/Makefile
 create mode 100644 src/versions/native/structures.ml

(limited to 'src/versions/native')

diff --git a/src/versions/native/Make b/src/versions/native/Make
new file mode 100644
index 0000000..75758b2
--- /dev/null
+++ b/src/versions/native/Make
@@ -0,0 +1,96 @@
+########################################################################
+##   This file is intended to developers, please do not use it to     ##
+## generate a Makefile, rather use the provided Makefile.             ##
+########################################################################
+
+
+
+
+########################################################################
+## To generate the Makefile:                                          ##
+##   coq_makefile -f Make -o Makefile                                 ##
+## Change the "all" target into:                                      ##
+##   all: ml $(CMXFILES) $(CMXA) $(CMXS) $(VOFILES)                   ##
+## Change the "install-natdynlink" target: change CMXSFILES into CMXS and add the same thing for CMXA and VCMXS. ##
+## Change the "install" target: change CMO into CMX.                  ##
+## Finally, suppress the "Makefile" target and add to the "clean" target: ##
+##   - 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 ##
+########################################################################
+
+
+-R . SMTCoq
+
+-I cnf
+-I euf
+-I lia
+-I smtlib2
+-I trace
+-I verit
+-I zchaff
+-I versions/native
+
+-custom "cd ../unit-tests; make" "" "test"
+-custom "cd ../unit-tests; make zchaff" "" "ztest"
+-custom "cd ../unit-tests; make verit" "" "vtest"
+
+-custom "$(CAMLLEX) $<" "%.mll" "%.ml"
+-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) -o $@ -linkall -shared $^" "$(CMXA)" "$(CMXS)"
+
+CMXA = trace/smtcoq.cmxa
+CMXS = trace/smt_tactic.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_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.cmxs 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
+
+versions/native/structures.ml
+
+trace/coqTerms.ml
+trace/satAtom.ml
+trace/smtAtom.ml
+trace/smtAtom.mli
+trace/smtCertif.ml
+trace/smtCnf.ml
+trace/smtCommands.ml
+trace/smtForm.ml
+trace/smtForm.mli
+trace/smtMisc.ml
+trace/smt_tactic.ml4
+trace/smtTrace.ml
+
+smtlib2/smtlib2_parse.ml
+smtlib2/smtlib2_lex.ml
+smtlib2/smtlib2_ast.ml
+smtlib2/smtlib2_genConstr.ml
+smtlib2/smtlib2_util.ml
+
+verit/veritParser.ml
+verit/veritLexer.ml
+verit/verit.ml
+verit/veritSyntax.ml
+verit/veritSyntax.mli
+
+zchaff/cnfParser.ml
+zchaff/satParser.ml
+zchaff/zchaff.ml
+zchaff/zchaffParser.ml
+
+cnf/Cnf.v
+
+euf/Euf.v
+
+lia/lia.ml
+lia/Lia.v
+
+spl/Syntactic.v
+spl/Arithmetic.v
+spl/Operators.v
+
+Misc.v
+SMTCoq.v
+SMT_terms.v
+State.v
+Trace.v
diff --git a/src/versions/native/Makefile b/src/versions/native/Makefile
new file mode 100644
index 0000000..5ab7a2d
--- /dev/null
+++ b/src/versions/native/Makefile
@@ -0,0 +1,435 @@
+#############################################################################
+##  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_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.cmxs 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\
+  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/versions/native/structures.ml b/src/versions/native/structures.ml
new file mode 100644
index 0000000..28ad7e2
--- /dev/null
+++ b/src/versions/native/structures.ml
@@ -0,0 +1,72 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+open Entries
+open Coqlib
+
+
+
+let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant)
+
+
+
+(* Int63 *)
+let int63_modules = [["Coq";"Numbers";"Cyclic";"Int63";"Int63Native"]]
+
+let mkInt : int -> Term.constr =
+  fun i -> Term.mkInt (Uint63.of_int i)
+
+let cint = gen_constant int63_modules "int"
+
+(* PArray *)
+let parray_modules = [["Coq";"Array";"PArray"]]
+
+let max_array_size : int =
+  Parray.trunc_size (Uint63.of_int 4194303)
+let mkArray : Term.types * Term.constr array -> Term.constr =
+  Term.mkArray
+
+
+(* Differences between the two versions of Coq *)
+let dummy_loc = Pp.dummy_loc
+
+let mkConst c =
+  { const_entry_body = c;
+    const_entry_type = None;
+    const_entry_secctx = None;
+    const_entry_opaque = false;
+    const_entry_inline_code = false}
+
+let error = Errors.error
+
+let coqtype = lazy Term.mkSet
+
+let declare_new_type t =
+  Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) (Lazy.force coqtype) [] false None (dummy_loc, t);
+  Term.mkVar t
+
+let declare_new_variable v constr_t =
+  Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) constr_t [] false None (dummy_loc, v);
+  Term.mkVar v
+
+let extern_constr = Constrextern.extern_constr true Environ.empty_env
+
+let vernacentries_interp expr =
+  Vernacentries.interp (Vernacexpr.VernacCheckMayEval (Some (Glob_term.CbvVm None), None, expr))
+
+let pr_constr_env = Printer.pr_constr_env
+
+let lift = Term.lift
-- 
cgit