diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-30 03:03:50 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-30 03:03:50 +0200 |
| commit | 98bf2facf5a61758897d000c4a7d1d6c6c2965fb (patch) | |
| tree | fcb99694bdc0df548398a718676847acdc5436c3 /src/versions/native/Makefile | |
| parent | 640bf0dda4a4880aeb525d1460dc91f5041aa626 (diff) | |
| download | smtcoq-98bf2facf5a61758897d000c4a7d1d6c6c2965fb.tar.gz smtcoq-98bf2facf5a61758897d000c4a7d1d6c6c2965fb.zip | |
Holes in proof:
- can now take learned clauses as argument
- returns a whole clause (and not only a literal)
- tested for the vernacular commands
Warning: seems to slow down 8.5 version
Diffstat (limited to 'src/versions/native/Makefile')
| -rw-r--r-- | src/versions/native/Makefile | 3 |
1 files changed, 2 insertions, 1 deletions
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 |