aboutsummaryrefslogtreecommitdiffstats
path: root/src/versions/native/Make
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@lri.fr>2016-09-23 16:01:42 +0200
committerChantal Keller <Chantal.Keller@lri.fr>2016-09-23 16:01:42 +0200
commit4be43131e2b3dc60a530de5b3a8f23cd93564ad7 (patch)
tree7743e1fbae5ee7b7ae72b16d35ea7fa38a9e46f2 /src/versions/native/Make
parentfa9d33eea03bb59d55ee4dccf4fecb8b1520e69d (diff)
downloadsmtcoq-4be43131e2b3dc60a530de5b3a8f23cd93564ad7.tar.gz
smtcoq-4be43131e2b3dc60a530de5b3a8f23cd93564ad7.zip
More modularity on the format of traces depending on the version of coq
Diffstat (limited to 'src/versions/native/Make')
-rw-r--r--src/versions/native/Make3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/versions/native/Make b/src/versions/native/Make
index 2b81917..07ff232 100644
--- a/src/versions/native/Make
+++ b/src/versions/native/Make
@@ -42,10 +42,11 @@
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"
+VCMXS = "versions/native/NSMTCoq_versions_native_Structures.cmxs 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
+versions/native/Structures.v
versions/native/structures.ml
trace/coqTerms.ml