diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-06-21 18:57:33 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-06-21 18:57:33 +0100 |
| commit | 4d262face34cb79d478823fd8db32cf02dc187f8 (patch) | |
| tree | 820335def3dc6d2fda3b779e8079b0c5fac8620c /Makefile | |
| parent | 323f262727ac3a4b129bdaeaa21083d8daa5184c (diff) | |
| download | vericert-4d262face34cb79d478823fd8db32cf02dc187f8.tar.gz vericert-4d262face34cb79d478823fd8db32cf02dc187f8.zip | |
Add SMTCoq solver as dependency
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 18 |
1 files changed, 2 insertions, 16 deletions
@@ -15,22 +15,8 @@ COQINCLUDES := -R src vericert \ $(foreach d, $(COMPCERTRECDIRS), -R lib/CompCert/$(d) compcert.$(d)) \ -R lib/CompCert/flocq Flocq \ -R lib/CompCert/MenhirLib MenhirLib \ - -R src TVSMT \ - -R lib/cohpred/smtcoq/src SMTCoq \ - -I lib/smtcoq/src \ - -I lib/smtcoq/src/bva \ - -I lib/smtcoq/src/classes \ - -I lib/smtcoq/src/array \ - -I lib/smtcoq/src/cnf \ - -I lib/smtcoq/src/euf \ - -I lib/smtcoq/src/lfsc \ - -I lib/smtcoq/src/lia \ - -I lib/smtcoq/src/smtlib2 \ - -I lib/smtcoq/src/trace \ - -I lib/smtcoq/src/verit \ - -I lib/smtcoq/src/zchaff \ - -I lib/smtcoq/src/PArray \ - -I lib/smtcoq/src/../3rdparty/alt-ergo + -R lib/cohpred/theory cohpred_theory \ + -R lib/cohpred/smtcoq/src SMTCoq COQEXEC := $(COQBIN)coqtop $(COQINCLUDES) -batch -load-vernac-source |