diff options
| author | bertot | 2001-04-04 12:52:09 +0000 |
|---|---|---|
| committer | bertot | 2001-04-04 12:52:09 +0000 |
| commit | 592e0bb0d9b3560c5ddc380e2fd5e58cbdac40ef (patch) | |
| tree | 82d1e8190ba62ed8ab9a77c881d16acec6ab484b | |
| parent | 085807162a7acf72fc060f3720eef43eacde7fe5 (diff) | |
add the compilation of the files needed for the interface with pcoq.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1535 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile | 15 |
1 files changed, 14 insertions, 1 deletions
@@ -40,7 +40,9 @@ noargument: LOCALINCLUDES= -I config -I tools -I scripts -I lib -I kernel -I library \ -I proofs -I tactics -I pretyping -I parsing -I toplevel \ -I contrib/omega -I contrib/ring -I contrib/xml \ - -I contrib/extraction -I contrib/correctness + -I contrib/extraction -I contrib/correctness \ + -I contrib/interface + INCLUDES=$(LOCALINCLUDES) -I $(CAMLP4LIB) BYTEFLAGS=-rectypes $(INCLUDES) $(CAMLDEBUG) @@ -151,6 +153,14 @@ CORRECTNESS=contrib/correctness/pmisc.cmo \ contrib/correctness/pwp.cmo contrib/correctness/pmlize.cmo \ contrib/correctness/ptactic.cmo contrib/correctness/psyntax.cmo +INTERFACE=contrib/interface/vtp.cmo contrib/interface/xlate.cmo \ + contrib/interface/paths.cmo contrib/interface/translate.cmo \ + contrib/interface/pbp.cmo \ + contrib/interface/dad.cmo \ + contrib/interface/history.cmo \ + contrib/interface/name_to_ast.cmo contrib/interface/debug_tac.cmo \ + contrib/interface/centaur.cmo + ML4FILES += contrib/correctness/psyntax.ml4 CONTRIB=contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \ @@ -238,6 +248,9 @@ toplevel: $(TOPLEVEL) bin/coq-extraction: $(COQMKTOP) $(CMO) $(USERTACCMO) $(EXTRACTIONCMO) $(COQMKTOP) -top $(INCLUDES) $(CAMLDEBUG) -o $@ $(EXTRACTIONCMO) +bin/coq-interface: $(COQMKTOP) $(CMO) $(USERTACCMO) $(INTERFACE) + $(COQMKTOP) -top $(INCLUDES) $(CAMLDEBUG) -o $@ $(INTERFACE) + ########################################################################### # tests ########################################################################### |