Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Raphaël Cauderlier
math_transfer
Commits
cad483e2
Commit
cad483e2
authored
Mar 26, 2017
by
Raphael Cauderlier
Browse files
Fix interop/logic/Makefile: Coq.Init.Peano is required in interop/arith/
parent
c8bf4e76
Changes
1
Hide whitespace changes
Inline
Side-by-side
interop/logic/Makefile
View file @
cad483e2
...
...
@@ -4,7 +4,7 @@ include ../../Makefile.rules
FCL_FILES
=
$(
wildcard
*
.fcl
)
V_FILES
=
$(
wildcard
*
.v
)
DK_FILES
=
$(
wildcard
*
.dk
)
all
:
$(FCL_FILES:.fcl=.dko) $(V_FILES:.v=.dko) $(DK_FILES:.dk=.dko) Coq__Init__Datatypes.dko
all
:
$(FCL_FILES:.fcl=.dko) $(V_FILES:.v=.dko) $(DK_FILES:.dk=.dko) Coq__Init__Datatypes.dko
Coq__Init__Peano.dko
INCLUDE_DIRS
=
-I
../../core/logic
...
...
@@ -21,11 +21,14 @@ holtypes.dk: dks_from_coqine
Coq__Init__Logic.dk
:
dks_from_coqine
Coq__Init__Wf.dk
:
dks_from_coqine
Coq__Init__Datatypes.dk
:
dks_from_coqine
Coq__Init__Peano.dk
:
dks_from_coqine
holtypes.dko
:
holtypes.dk Coq.dko
# TODO: automate dependency computation of Coqine-generated files
Coq__Init__Logic.dko
:
Coq__Init__Logic.dk Coq.dko
Coq__Init__Datatypes.dko
:
Coq__Init__Datatypes.dk Coq.dko Coq__Init__Logic.dko
Coq__Init__Wf.dko
:
Coq__Init__Wf.dk Coq.dko Coq__Init__Logic.dko Coq__Init__Datatypes.dko
Coq__Init__Peano.dko
:
Coq__Init__Peano.dk Coq.dko Coq__Init__Logic.dko Coq__Init__Datatypes.dko
Coq__Init__Wf.dko
:
Coq__Init__Wf.dk Coq.dko Coq__Init__Logic.dko Coq__Init__Datatypes.dko Coq__Init__Peano.dko
# Dependencies between the dk/dko files could be automatised as
# $(DKDEP) $(INCLUDE_DIRS) >> $@ but only starting with Dedukti v2.6
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment