diff options
| author | ckeller <ckeller@users.noreply.github.com> | 2019-02-14 20:09:40 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-02-14 20:09:40 +0100 |
| commit | ec41af7ac01cef7c30785e6dd704381f31e7c2d3 (patch) | |
| tree | 13d51483c50d7b5a668d90b8b67a8b99ef0fbe56 /src/versions/standard/Make | |
| parent | ba22fad2fb46962eef5f30d976e9eaeb587023a0 (diff) | |
| download | smtcoq-ec41af7ac01cef7c30785e6dd704381f31e7c2d3.tar.gz smtcoq-ec41af7ac01cef7c30785e6dd704381f31e7c2d3.zip | |
V8.7 (#36)
Port SMTCoq to Coq-8.7
Diffstat (limited to 'src/versions/standard/Make')
| -rw-r--r-- | src/versions/standard/Make | 12 |
1 files changed, 3 insertions, 9 deletions
diff --git a/src/versions/standard/Make b/src/versions/standard/Make index ee7f119..e47c530 100644 --- a/src/versions/standard/Make +++ b/src/versions/standard/Make @@ -10,14 +10,8 @@ ## To generate the Makefile: ## ## coq_makefile -f Make -o Makefile ## ## In the Makefile : ## -## 1) Suppress the "Makefile" target ## -## 2) Change the "all" target: ## -## remove the "test", "ztest", "vtest", "lfsctest" and "./" ## -## dependencies ## -## 3) Change the "install" and "clean" targets: ## -## Suppress the "+" lines ## -## 4) Add to the "clean" target: ## -## - rm -f ../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 smtlib2/sExprParser.mli smtlib2/sExprParser.ml smtlib2/sExprLexer.ml ## +## 1) Add "-native" to the CAMLDEP command (ocamldep -native ...) ## +## 2) remove "post-all" from the targets "all" and "all.timing.diff" ## ######################################################################## @@ -41,7 +35,7 @@ -I "$(shell $(COQBIN)coqc -where)/plugins/micromega" --extra "test" "" "cd ../unit-tests; make" "" +-extra "test" "" "cd ../unit-tests; make" -extra "ztest" "" "cd ../unit-tests; make zchaff" -extra "vtest" "" "cd ../unit-tests; make verit" -extra "lfsctest" "" "cd ../unit-tests; make lfsc" |