aboutsummaryrefslogtreecommitdiffstats
path: root/src/versions
diff options
context:
space:
mode:
Diffstat (limited to 'src/versions')
-rw-r--r--src/versions/native/Make3
-rw-r--r--src/versions/native/Makefile3
-rw-r--r--src/versions/standard/Make1
-rw-r--r--src/versions/standard/Makefile63
4 files changed, 61 insertions, 9 deletions
diff --git a/src/versions/native/Make b/src/versions/native/Make
index 75758b2..5659cc7 100644
--- a/src/versions/native/Make
+++ b/src/versions/native/Make
@@ -42,7 +42,7 @@
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"
+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
@@ -85,6 +85,7 @@ euf/Euf.v
lia/lia.ml
lia/Lia.v
+spl/Assumptions.v
spl/Syntactic.v
spl/Arithmetic.v
spl/Operators.v
diff --git a/src/versions/native/Makefile b/src/versions/native/Makefile
index 5ab7a2d..c7ac7c5 100644
--- a/src/versions/native/Makefile
+++ b/src/versions/native/Makefile
@@ -65,7 +65,7 @@ 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_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
+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
@@ -142,6 +142,7 @@ VFILES:=Trace.v\
spl/Operators.v\
spl/Arithmetic.v\
spl/Syntactic.v\
+ spl/Assumptions.v\
lia/Lia.v\
euf/Euf.v\
cnf/Cnf.v
diff --git a/src/versions/standard/Make b/src/versions/standard/Make
index 4d548ad..42d0552 100644
--- a/src/versions/standard/Make
+++ b/src/versions/standard/Make
@@ -99,6 +99,7 @@ euf/Euf.v
lia/lia.ml
lia/Lia.v
+spl/Assumptions.v
spl/Syntactic.v
spl/Arithmetic.v
spl/Operators.v
diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile
index 33ce492..cb92e59 100644
--- a/src/versions/standard/Makefile
+++ b/src/versions/standard/Makefile
@@ -2,7 +2,7 @@
## v # The Coq Proof Assistant ##
## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
## \VV/ # ##
-## // # Makefile automagically generated by coq_makefile V8.5 ##
+## // # Makefile automagically generated by coq_makefile V8.5pl1 ##
#############################################################################
# WARNING
@@ -96,12 +96,22 @@ COQDOC?="$(COQBIN)coqdoc"
COQCHK?="$(COQBIN)coqchk"
COQMKTOP?="$(COQBIN)coqmktop"
-COQSRCLIBS?=-I "$(COQLIB)kernel" -I "$(COQLIB)lib" \
- -I "$(COQLIB)library" -I "$(COQLIB)parsing" -I "$(COQLIB)pretyping" \
- -I "$(COQLIB)interp" -I "$(COQLIB)printing" -I "$(COQLIB)intf" \
- -I "$(COQLIB)proofs" -I "$(COQLIB)tactics" -I "$(COQLIB)tools" \
- -I "$(COQLIB)toplevel" -I "$(COQLIB)stm" -I "$(COQLIB)grammar" \
- -I "$(COQLIB)config" \
+COQSRCLIBS?=-I "$(COQLIB)kernel" \
+-I "$(COQLIB)lib" \
+-I "$(COQLIB)library" \
+-I "$(COQLIB)parsing" \
+-I "$(COQLIB)pretyping" \
+-I "$(COQLIB)interp" \
+-I "$(COQLIB)printing" \
+-I "$(COQLIB)intf" \
+-I "$(COQLIB)proofs" \
+-I "$(COQLIB)tactics" \
+-I "$(COQLIB)tools" \
+-I "$(COQLIB)toplevel" \
+-I "$(COQLIB)stm" \
+-I "$(COQLIB)grammar" \
+-I "$(COQLIB)config" \
+ \
-I "$(COQLIB)/plugins/btauto" \
-I "$(COQLIB)/plugins/cc" \
-I "$(COQLIB)/plugins/decl_mode" \
@@ -168,6 +178,7 @@ VFILES:=versions/standard/Int63/Int63.v\
cnf/Cnf.v\
euf/Euf.v\
lia/Lia.v\
+ spl/Assumptions.v\
spl/Syntactic.v\
spl/Arithmetic.v\
spl/Operators.v\
@@ -413,6 +424,44 @@ uninstall_me.sh: Makefile
uninstall: uninstall_me.sh
sh $<
+.merlin:
+ @echo 'FLG -rectypes' > .merlin
+ @echo "B $(COQLIB) kernel" >> .merlin
+ @echo "B $(COQLIB) lib" >> .merlin
+ @echo "B $(COQLIB) library" >> .merlin
+ @echo "B $(COQLIB) parsing" >> .merlin
+ @echo "B $(COQLIB) pretyping" >> .merlin
+ @echo "B $(COQLIB) interp" >> .merlin
+ @echo "B $(COQLIB) printing" >> .merlin
+ @echo "B $(COQLIB) intf" >> .merlin
+ @echo "B $(COQLIB) proofs" >> .merlin
+ @echo "B $(COQLIB) tactics" >> .merlin
+ @echo "B $(COQLIB) tools" >> .merlin
+ @echo "B $(COQLIB) toplevel" >> .merlin
+ @echo "B $(COQLIB) stm" >> .merlin
+ @echo "B $(COQLIB) grammar" >> .merlin
+ @echo "B $(COQLIB) config" >> .merlin
+ @echo "B cnf" >> .merlin
+ @echo "S cnf" >> .merlin
+ @echo "B euf" >> .merlin
+ @echo "S euf" >> .merlin
+ @echo "B lia" >> .merlin
+ @echo "S lia" >> .merlin
+ @echo "B smtlib2" >> .merlin
+ @echo "S smtlib2" >> .merlin
+ @echo "B trace" >> .merlin
+ @echo "S trace" >> .merlin
+ @echo "B verit" >> .merlin
+ @echo "S verit" >> .merlin
+ @echo "B zchaff" >> .merlin
+ @echo "S zchaff" >> .merlin
+ @echo "B versions/standard" >> .merlin
+ @echo "S versions/standard" >> .merlin
+ @echo "B versions/standard/Int63" >> .merlin
+ @echo "S versions/standard/Int63" >> .merlin
+ @echo "B versions/standard/Array" >> .merlin
+ @echo "S versions/standard/Array" >> .merlin
+
clean::
rm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES)
rm -f $(ALLCMOFILES:.cmo=.cmx) $(CMXAFILES) $(CMXSFILES) $(ALLCMOFILES:.cmo=.o) $(CMXAFILES:.cmxa=.a)
generated by cgit (git 2.34.1) at 2024-07-03 09:30:50 +0000